FORMATS-FTRTFT 2004 START ConferenceManager    

Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications

Felix C. Gärtner and Arshad Jhumka

Presented at Formal Modelling and Analysis of Timed Systems - Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT 2004), Grenoble, France, September 22-24, 2004


The fault tolerance theories by Arora and Kulkarni and by Jhumka et al. view a fault-tolerant program as the result of composing a fault-intolerant program with fault tolerance components called detectors and correctors. At their core, the theories assume that the correctness specifications under consideration are fusion closed. In general, fusion closure of specifications can be achieved by adding history variables to the program. However, addition of history variables causes an exponential growth of the state space of the program, causing addition of fault tolerance to be expensive. To redress this problem, we present a method which can be used to add history information to a program in a way that significantly reduces the number of additional states. Hence, automated methods that add fault tolerance can now be efficiently applied in environments where specifications are not necessarily fusion closed.

START Conference Manager (V2.47.2)