Access Restriction

Author Kumar, D. ♦ Iyengar, S.S.
Source IEEE Xplore Digital Library
Content type Text
Publisher Institute of Electrical and Electronics Engineers, Inc. (IEEE)
File Format PDF
Copyright Year ©1997
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Broadcasting ♦ Algorithm design and analysis ♦ Safety ♦ Distributed algorithms ♦ System recovery ♦ Message passing ♦ Cities and towns ♦ Educational institutions ♦ Distributed databases ♦ Computer science
Abstract In past years, a large number of published distributed algorithms have been shown to be incorrect. Unfortunately, designers of distributed algorithms typically use informal correctness proofs, which tend to be unreliable. Formal correctness proofs offer a much higher degree of reliability, but they are not popular among algorithm designers because they are too mathematical and they typically assume synchronous message communication or some other abstract notation, and are therefore not easily applicable to the asynchronous message passing environment, the environment commonly assumed by many algorithm designers. To address this problem, we have developed a semiformal correctness proof method for the asynchronous message passing environment, using ideas from well known formal correctness proof methods. We illustrate part of the proof method by proving the safety property of a simple network broadcast algorithm.
Description Author affiliation: Dept. of Comput. Sci., City Univ. of New York, NY, USA (Kumar, D.)
ISBN 0818681055
ISSN 07303157
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research ♦ Reading
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1997-08-13
Publisher Place USA
Rights Holder Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Size (in Bytes) 416.27 kB
Page Count 4
Starting Page 668
Ending Page 671

Source: IEEE Xplore Digital Library