Weakest Invariant Generation for Automated Addition of Fault-Tolerance

Fuad Abujarad and Sandeep S. Kulkarni


One of the important tasks in evolving a fault-intolerant program into a fault-tolerant one is to identify the legitimate states (its invariant) from where the original program satisfies its specification. This allows us to ensure that the fault-tolerant program recovers to these legitimate states from where it satisfies its specification. It is desired that the invariant be the weakest possible so as to provide maximal options to the algorithm for adding fault-tolerance. Requiring the designer to specify such weak invariant increases the burden on the designer. In this paper, we present a novel approach for automating the generation of the weakest invariant from the program actions and specifications. Our algorithm is efficient and manages the state explosion problem with the use of BDDs. We demonstrate our approach through two case studies and we show that generating such invariants is extremely fast. For example, for a mutual exclusion program with a state space of size 10^{84} states, it took 0.9 of a second.


Return to the publication list
Return to the Sandeep's home page