Machine checked proofs of the design of a fault-tolerant circuit

Publisher Website
Google Scholar
Abstract
We describe a formally verified implementation of the “Oral Messages” algorithm of Pease, Shostak and Lamport J. ACM (1980) 27 , 228–234; ACM TOPLAS (1982) 4 , 382–401. An abstract implementation of the algorithm is proved to achieve interactive consistency in the presence of faults. This abstract characterisation is then mapped down to a hardware level implementation which inherits the fault-tolerant characteristics of the abstract version. All steps in the proof were checked with the Boyer-Moore theorem prover. A significant result of this work is the demonstration of a fault-tolerant device that is formally specified and the development of an implementation proved correct with respect to this specification. A significant simplifying assumption is that the redundant processors behave synchronously. We also describe a mechanically checked proof that the Oral Messages algorithm is “optimal” in the sense that no algorithm which achieves agreement via similar message passing can tolerate a larger proportion of faulty processors.

This publication has 5 references indexed in Scilit: