Year of Publication
International Symposium on Formal Methods (FM)
The problem of enforcing bounded-time 2-phase recovery in real-time programs is often necessitated by conflict between fault-tolerance requirements and timing constraints. In this paper, we address the problem of synthesizing two types of 2-phase recovery: relaxed and graceful. Intuitively, relaxed 2-phase recovery requires that in the presence of faults, the program recovers to an acceptable behavior within some time θ and recovers to ideal behavior within time δ. And, graceful 2-phase recovery allows us to capture a requirement that the time to recover from faults is proportional to the perturbation caused by that fault. We show that the problem of synthesizing relaxed bounded-time 2-phase recovery is NP-complete although a similar problem of graceful 2-phase recovery can be solved in polynomial-time both in the size of the input program’s region graph. Finally, based on the results in this paper, we argue that the requirement of intermediate recording of a fault before reaching legitimate states can increase the complexity of adding fault-tolerance substantially.