Weakest Invariant Generation for Automated Addition of Fault-Tolerance
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 one 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. This paper presents a novel approach for automating the generation of the weakest invariant from the program actions and specifications.