Specifying and Verifying Fault-Tolerant Systems

Leslie Lamport, Stephan Merz

Abstract

We formally specify a well-known solution to the Byzantine generals problem and give a rigorous, hierarchically structured proof of its correctness. We demonstrate that this is an engineering exercise, requiring no new scientific ideas.

Available as:  gzip'ed Postscript 

Reference

@INPROCEEDINGS(lamport:fault,
   TITLE = "Specifying and Verifying  Fault-Tolerant Systems",
   AUTHOR = "Leslie Lamport and Stephan Merz",
   PuBlIsHeR = "Springer-Verlag",
   BOOKTITLE = "Formal Techniques in Real-Time and 
                Fault-Tolerant Systems",
   month = sep,
   YEAR = 1994,
   editor = "H. Langmaack and W.-P. de Roever and J. Vytopil",
   series = "Lecture Notes in Computer Science",
   volume = "863",
   pages = "41--76"
)