Title :
Comparing verification systems: interactive consistency in ACL2
Author :
Young, William D.
Author_Institution :
Comput. Logic Inc., Austin, TX, USA
Abstract :
Achieving interactive consistency among processors in the presence of faults is an important problem in fault-tolerant computing, first cleanly formulated by Pease, Shostak and Lamport (1980) and solved in selected cases with their Oral Messages (OM) algorithm. Several mechanical verifications of this algorithm have been presented, including a particularly elegant formulation and proof by J. Rushby (1992) using EHDM and PVS. Rushby proposes interactive consistency as a benchmark problem for specification and verification systems. We present a formalization of the OM algorithm in the ACL2 logic and compare our formalization and proof to his. We draw some conclusions concerning the range of desirable features for verification systems and offer a cautionary note about relying on such benchmark problems when comparing systems
Keywords :
LISP; fault tolerant computing; formal logic; formal specification; formal verification; interactive systems; program verification; ACL2 logic; EHDM; Oral Messages algorithm; PVS; algorithm verification; benchmark problem; desirable features; fault-tolerant computing; formalization; inter-processor consistency; interactive consistency; specification systems; verification systems comparison; Algorithm design and analysis; Fault tolerance; Fault tolerant systems; Logic;
Conference_Titel :
Computer Assurance, 1996. COMPASS '96, Systems Integrity. Software Safety. Process Security. Proceedings of the Eleventh Annual Conference on
Conference_Location :
Gaithersburg, MD
Print_ISBN :
0-7803-3390-X
DOI :
10.1109/CMPASS.1996.507873
