This Article 
 Bibliographic References 
 Add to: 
Comparing Verification Systems: Interactive Consistency in ACL2
April 1997 (vol. 23 no. 4)
pp. 214-223

Abstract—Achieving interactive consistency 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.

[1] W.R. Bevier and W.D. Young, "The Proof of Correctness of a Fault-Tolerant Circuit Design," Proc. Second Int'l Working Conf. Dependable Computing for Critical Applications, pp. 107-114, IFIP Feb. 1991.
[2] W.R. Bevier and W.D. Young, "Machine Checked Proofs of the Design of a Fault-Tolerant Circuit," Formal Aspects of Computing, vol. 4, pp. 755-775, 1992.
[3] R.S. Boyer and J S. Moore, "The Addition of Bounded Quantification and Partial Functions to A Computational Logic and its Theorem Prover," Technical Report ICSCA-CMP-52, Institute for Computing Science, Univ. of Texas at Austin, Jan. 1987.
[4] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[5] R.W. Butler, "An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot," Technical Memorandum 110255, NASA, May, 1996.
[6] K. Finney, "Mathematical Notation in Formal Specification: Too Difficult for the Masses?" IEEE Trans. Software Eng., vol. 22, no. 2, pp. 158-159, Feb. 1996.
[7] M. Kaufmann and J S. Moore, "Design Goals for ACL2," Proc. Third Int'l School and Symp. Formal Techniques in Real Time and Fault Tolerant Systems, pp. 92-117, Christian-Albrechts Universitat, 1994.
[8] L. Lamport, "Types Considered Harmful," Internal note, DEC Systems Research Center, Dec. 1992.
[9] L. Lamport, R. Shostak, and M. Pease, "The Byzantine Generals Problem," ACM Trans. Programming Languages and Systems, vol. 4, no. 3, July 1982, pp. 382-401.
[10] J S. Moore, "Mechanically Verified Hardware Implementing an 8-Bit Parallel IO Byzantine Agreement Processor," Technical Report 69, Computational Logic, Inc., Aug. 1991.
[11] J S. Moore and M. Kaufmann, "An Industrial Strength Theorem Prover for a Logic Based on Common Lisp," Trans. Software Eng., Apr. 1997.
[12] S. Owre, J. Rushby, N. Shankar, and F. von Henke, "Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS," IEEE Trans. Software Eng., vol. 21, pp. 107-125, Feb. 1995.
[13] S. Owre, J.M. Rushby, and N. Shankar, "PVS: A Prototype Verification System," E. Kapur, ed., Proc. 11th Conf. Automated Deduction, Lecture Notes in Computer Science 607. Springer-Verlag, 1992.
[14] M. Pease, R. Shostak, and L. Lamport, “Reaching Agreement in the Presence of Faults,” J. ACM, vol. 27, no. 2, pp. 228–234, Apr. 1980.
[15] J. Rushby, “Formal Verification of an Oral Messages Algorithm for Interactive Consistency,” Technical Report SRI-CSL-92-1, Computer Science Laboratory, SRI Int'l, Menlo Park, Calif., July 1992. also available as NASA Contractor Report 189704, Oct. 1992.
[16] J. Rushby, "Formal Methods and their Role in Certification of Critical Systems," Technical Report CSL-95-1, Computer Science Laboratory, SRI Int'l, Mar. 1995.
[17] J. Rushby, "Formal Methods and their Role in Digital Systems Validation for Airborne Systems," Contractor Report, number 4673, NASA, Aug. 1995.
[18] J. Rushby and F. von Henke, "Formal Verification of the Interactive Convergence Clock Synchronization Algorithm using EHDM," Technical report, Computer Science Laboratory, SRI Int'l, Menlo Park, Calif., Jan. 1989.
[19] J. Rushby, F. von Henke, and S. Owre, "An Introduction to Formal Specification and Verification using EHDM, Technical Report SRI-CSL-91-2, Computer Science Laboratory, SRI Int'l, Feb. 1991.
[20] L. Wos and S. Winker, "Open Questions Solved with the Assistance of AURA," Automatic Theorem Proving: After 25 Years. D. Loveland and W.W. Bledsoe, eds., Am. Mathe. Soc., 1984.
[21] W.D. Young, "Verifying the Interactive Convergence Clock Synchronization Algorithm Using the Boyer-Moore Theorem Prover," Contractor Report 189649, NASA, Apr. 1992.
[22] W.D. Young, "Specification of a Simple Autopilot in ACL2," Internal Note 327, Computational Logic, Inc., July 1996.
[23] W.D. Young and W.R. Bevier, "Mathematical Modeling and Analysis of an External Memory Manager," Technical Report 105, Computational Logic, Inc., Oct. 1994.

Index Terms:
Formal verification, automatic theorem proving, fault tolerance, computational logic, specification languages.
William D. Young, "Comparing Verification Systems: Interactive Consistency in ACL2," IEEE Transactions on Software Engineering, vol. 23, no. 4, pp. 214-223, April 1997, doi:10.1109/32.588536
Usage of this product signifies your acceptance of the Terms of Use.