SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Formal Verification of an Oral Messages Algorithm for Interactive Consistency
 by Dr. John Rushby.

Number SRI-CSL-92-1.
Computer Science Laboratory, SRI International, Menlo Park, CA.
July, 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.

BibTEX Entry
@techreport{csl-92-1,
    AUTHOR = {John Rushby},
    TITLE = {Formal Verification of an Oral Messages Algorithm for Interactive Consistency},
    INSTITUTION = {Computer Science Laboratory, {SRI} International},
    YEAR = {1992},
    NUMBER = {{SRI-CSL-92-1}},
    ADDRESS = {Menlo Park, {CA}},
    MONTH = {jul},
    NOTE = {Also available as {NASA} Contractor Report 189704, October 1992},
    URL = {http://www.csl.sri.com/papers/csl-92-1/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy