loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2004 International Conference on Dependable Systems and Networks (DSN'04)
Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation
Florence, Italy
June 28-July 01
ISBN: 0-7695-2052-9
Wilfried Steiner, Technische Universit?t Wien, Austria
John Rushby, SRI International, USA
Maria Sorea, Universit?t Ulm, Germany
Holger Pfeifer, Universit?t Ulm, Germany
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 to automatically 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 capabilities of tools such as this.
Citation:
Wilfried Steiner, John Rushby, Maria Sorea, Holger Pfeifer, "Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation," dsn, pp.189, 2004 International Conference on Dependable Systems and Networks (DSN'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.