SAL Tutorial: Analyzing the Fault-Tolerant Algorithm OM(1)

John Rushby

CSL Technical Note

Abstract

The resources of SAL allow many kinds of systems to be modeled and analyzed. However, it requires skill and experience to exploit the capabilities of SAL to the best effect in any given problem domain. This tutorial provides an introduction to the use of SAL in modeling and analyzing fault-tolerant systems.

The example considered here is a simple variant on the classical one-round Oral Messages algorithm OM(1) for Byzantine agreement and will be familiar to many computer scientists. The SAL model developed here is available for download, so that users can repeat the analyses described, and exercises are suggested for additional experiments.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

SAL Files

om1.sal

Download SAL here

BibTeX Entry


@techreport{SAL-tut-om1,
        Author= {John Rushby},
        Title= {{SAL} Tutorial: Analyzing the Fault-Tolerant Algorithm {OM(1)}},
        TYPE = {CSL Technical Note},
        Institution= {Computer Science Laboratory, SRI International},
        Address= {Menlo Park, CA},
        Month= apr,
        Year= 2004,
	NOTE = {Available at \url{http://www.csl.sri.com/users/rushby/abstracts/om1}}
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page