Model Checking a Fault-Tolerant Startup Algorithm:
From Design Exploration To Exhaustive Fault Simulation

Wilfried Steiner, John Rushby, Maria Sorea, and Holger Pfeifer

Presented at DSN 04

Abstract

The increasing performance of modern model-checking tools offers high potential for the computer-aided design of fault-tolerant algorithms. Instead of relying on human imagination to generate taxing failure scenarios to probe a fault-tolerant algorithm during development, we define the fault behavior of a faulty process at its interfaces to the remaining system and use model checking automatically to examine all possible failure scenarios. We call this approach ``exhaustive fault simulation''. In this paper we illustrate exhaustive fault simulation using a new startup algorithm for the Time-Triggered Architecture (TTA) and show that this approach is fast enough to be deployed in the design loop. We use the SAL toolset from SRI for our experiments and describe an approach to modeling and analyzing fault-tolerant algorithms that exploits the capabilties of tools such as this.

This is the draft version: gzipped postscript, or plain postscript or pdf or crude ascii (for your Palm Pilot)

Here's the published version © IEEE PDF only.

BibTeX Entry

@inproceedings{Steiner-etal:DSN04,
	AUTHOR = {Wilfried Steiner and John Rushby and Maria Sorea and Holger Pfeifer},
	TITLE = {Model Checking a Fault-Tolerant Startup Algorithm:
		From Design Exploration To Exhaustive Fault Simulation},
	BOOKTITLE = {The International Conference on Dependable Systems and Networks},
	PAGES = {189--198},
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Florence, Italy},
	MONTH = jun,
	YEAR = 2004
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page