Incremental Synthesis of Fault-Tolerant Real-Time Programs

Borzoo Bonakdarpour and Sandeep S. Kulkarni


In this paper, we focus on the problem of automated addition of fault-tolerance to an existing fault-intolerant \emph{real-time}program. We consider three levels of fault-tolerance, namely \emph{nonmasking}, \emph{failsafe}, and \emph{masking}, based on safety and liveness properties satisfied in the presence of faults. More specifically, a nonmasking (respectively, failsafe, masking) program satisfies liveness (respectively, safety, both safety and liveness) in the presence of faults. For failsafe and masking fault-tolerance, we consider two additional levels, \emph{soft} and \emph{hard}, based on satisfaction of timing constraints in the presence of faults. We present a polynomial time algorithm (in the size of the input program's region graph) that adds \emph{bounded-time recovery} from an arbitrary given set of states to another arbitrary set of states. Using this algorithm, we propose a sound and complete synthesis algorithm that transforms a fault-intolerant real-time program into a nonmasking fault-tolerant program. Furthermore, we introduce sound and complete algorithms for adding soft/hard-failsafe fault-tolerance. For reasons of space, our results on addition of soft/hard-masking fault-tolerance are presented in a technical report.


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