Issue No. 04 - April (1997 vol. 23)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.588536
<p><b>Abstract</b>—Achieving <it>interactive consistency</it> among processors in the presence of faults is an important problem in fault tolerant computing, first cleanly formulated by Lamport, Pease, and Shostak and solved in selected cases with their Oral Messages (OM) algorithm. Several machine-supported verifications of this algorithm have been presented, including a particularly elegant formulation and proof by John Rushby 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. In particular, while higher-order functions, strong typing, lambda abstraction, and full quantification have some value they come with a cost; moreover, many uses of such features can be easily translated into simpler logical constructs, which facilitate more automated proof discovery. We offer a cautionary note about comparing systems with respect to a small set of problems in a limited domain.</p>
Formal verification, automatic theorem proving, fault tolerance, computational logic, specification languages.
W. D. Young, "Comparing Verification Systems: Interactive Consistency in ACL2," in IEEE Transactions on Software Engineering, vol. 23, no. , pp. 214-223, 1997.