The Proof of Correctness of a Fault-Tolerant Circuit Design

  • William R. Bevier
  • William D. Young
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 6)


We describe a formally verified implementation of the “Oral Messages” algorithm of Pease, Shostak, and Lamport. An abstract implementation of the algorithm has been verified to achieve interactive consistency in the presence of faults[1]. This abstract characterization is then mapped down to a hardware level design which inherits the fault-tolerant characteristics of the abstract version. The proof that the hardware level description is a correct implementation of the “Oral Messages” algorithm has been fully checked with a mechanical theorem prover. This design was then translated straightforwardly into a physical hardware implementation. A significant result of this work is the demonstration of a fault-tolerant device that is formally specified and whose implementation is proved correct with respect to this specification.


Circuit Design Trace Function Computational Logic Interactive Consistency Faulty Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    W. Bevier and W. Young, “Machine checked proofs of a Byzantine agreement algorithm,” Tech. Rep. 62, Computational Logic, Inc., June 1990.Google Scholar
  2. [2]
    M. Pease, R. Shostak, and L. Lamport, “Reaching agreement in the presence of faults,” JACM, vol. 27, pp. 228–234, April 1980.MathSciNetMATHCrossRefGoogle Scholar
  3. [3]
    L. Lamport, R. Shostak, and M. Pease, “The Byzantine generals problem,” ACM TOPLAS, vol. 4, pp. 382–401, July 1982.MATHCrossRefGoogle Scholar
  4. [4]
    R. Boyer and J. Moore, A Computational Logic. New York: Academic Press, 1979.MATHGoogle Scholar
  5. [5]
    R. Boyer and J. Moore, A Computational Logic Handbook. Boston: Academic Press, 1988.MATHGoogle Scholar
  6. [6]
    L. Claesen, Ed., Formal VLSI Specification and Synthesis. Amsterdam: North-Holland, 1990.Google Scholar
  7. [7]
    M. Lesser and G. Brown, Eds., Hardware Specification, Verification and Synthesis: Mathematical Aspects, vol. 408 of Lecture Notes in Computer Science. Berlin: Springer-Verlag, 1989.Google Scholar
  8. [8]
    J. Staunstrup, Ed., Formal Methods for VLSI Design. Amsterdam: North-Holland, 1990.MATHGoogle Scholar
  9. [9]
    M. Bickford and M. Srivas, “Formal verification of a fault-tolerant microprocessor system design,” contractor report, NASA, February 1991.Google Scholar

Copyright information

© Springer-Verlag/Wien 1992

Authors and Affiliations

  • William R. Bevier
    • 1
  • William D. Young
    • 1
  1. 1.Computational Logic, Inc.AustinUSA

Personalised recommendations