The Proof of Correctness of a Fault-Tolerant Circuit Design
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. 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.
KeywordsCircuit Design Trace Function Computational Logic Interactive Consistency Faulty Process
Unable to display preview. Download preview PDF.
- W. Bevier and W. Young, “Machine checked proofs of a Byzantine agreement algorithm,” Tech. Rep. 62, Computational Logic, Inc., June 1990.Google Scholar
- L. Claesen, Ed., Formal VLSI Specification and Synthesis. Amsterdam: North-Holland, 1990.Google Scholar
- 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
- M. Bickford and M. Srivas, “Formal verification of a fault-tolerant microprocessor system design,” contractor report, NASA, February 1991.Google Scholar