SRI International Computer Science Laboratory

Formal Verification of an Oral Messages Algorithm for Interactive Consistency

John Rushby

Technical Report CSL-92-01, July 1992

Also available as NASA Contractor Report 189704, October 1992

Abstract

We describe the formal specification and verification of an algorithm for Interactive Consistency based on the Oral Messages algorithm for Byzantine Agreement. We compare our treatment with that of Bevier and Young, who presented a formal specification and verification for a very similar algorithm. Unlike Bevier and Young, who observed that ``the invariant maintained in the recursive subcases of the algorithm is significantly more complicated than is suggested by the published proof'' and who found its formal verification ``a fairly difficult exercise in mechanical theorem proving,'' our treatment is very close to the previously published analysis of the algorithm, and our formal specification and verification are straightforward.

This example illustrates how delicate choices in the formulation of a problem can have significant impact on the readability of its formal specification and on the tractability of its formal verification.

dvi or postscript

New: PVS specification files for a treatment based on Appendix B are now available

PVS specification files
Return to the Formal Methods Program home page

Return to the Computer Science Laboratory home page