Paper Info
Title
Synthesizing bounded-time 2-phase fault recovery
Abstract
We focus on synthesis techniques for transforming existing fault-intolerant real-time programs into fault-tolerant programs that provide phased recovery. A fault-tolerant program is one that satisfies its safety and liveness specifications as well as timing constraints in the presence of faults. We argue that in many commonly considered programs (especially in safety/mission-critical systems), when faults occur, simple recovery to the program's normal behavior is necessary, but not sufficient. For such programs, it is necessary that recovery is accomplished in a sequence of phases, each ensuring that the program satisfies certain properties. In the simplest case, in the first phase the program recovers to an acceptable behavior within some time ¿, and, in the second phase, it recovers to the ideal behavior within time ¿. In this article, we introduce four different types of bounded-time 2-phase recovery, namely ordered-strict, strict, relaxed, and graceful, based on how a real-time fault-tolerant program reaches the acceptable and ideal behaviors in the presence of faults. We rigorously analyze the complexity of automated synthesis of each type: we either show that the problem is hard in some class of complexity or we present a sound and complete synthesis algorithm. We argue that such complexity analysis is essential to deal with the highly complex decision procedures of program synthesis.
Year
DOI
Venue
2015
10.1007/s00165-014-0325-8
Formal Asp. Comput.
Keywords
Field
DocType
bounded-time recovery,program transformation,program synthesis,phased recovery,real-time,fault-tolerance,fault tolerance,real time
Program transformation,Program synthesis,Computer science,Theoretical computer science,Fault tolerance,Program analysis,Bounded function,Liveness
Journal
Volume
Issue
ISSN
27
1
1433-299X
Citations 
PageRank 
References 
2
0.51
30
Authors
2
Name
Order
Citations
PageRank
Borzoo Bonakdarpour149045.02
Sandeep S. Kulkarni286379.94