Comparing verification systems: interactive consistency in ACL2

Author

Young, William D.

Author_Institution

Comput. Logic Inc., Austin, TX, USA

fYear

1996

fDate

17-21 Jun 1996

Firstpage

35

Lastpage

45

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/CMPASS.1996.507873

Filename

507873