caa a22 4500 605516103 CHVBK 20210128100712.0 cr unu---uuuuu 210128e20150101xx s 000 0 eng 10.1007/s00165-014-0325-8 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0325-8 Synthesizing bounded-time 2-phase fault recovery [Elektronische Daten] [Borzoo Bonakdarpour, Sandeep Kulkarni] 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. British Computer Society, 2014 Fault-tolerance nationallicence Real-time nationallicence Bounded-time recovery nationallicence Phased recovery nationallicence Program synthesis nationallicence Program transformation nationallicence Bonakdarpour Borzoo Department of Computing and Software, McMaster University, Hamilton, ON, Canada aut Kulkarni Sandeep Deparment of Computer Science and Engineering, Michigan State University, East Lansing, MI, USA aut Formal Aspects of Computing Springer London 27/1(2015-01-01), 1-31 0934-5043 27:1<1 2015 27 165 https://doi.org/10.1007/s00165-014-0325-8 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0325-8 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Bonakdarpour Borzoo Department of Computing and Software, McMaster University, Hamilton, ON, Canada aut NATIONALLICENCE 700 1- Kulkarni Sandeep Deparment of Computer Science and Engineering, Michigan State University, East Lansing, MI, USA aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/1(2015-01-01), 1-31 0934-5043 27:1<1 2015 27 165