Synthesizing and optimizing FDIR recovery strategies from fault trees

Redundancy concepts are major design drivers in fault-tolerant space systems. It can be a difficult task to decide when to activate which redundancy, and which component should be replaced. In this paper, we refine a methodology where recovery strategies are synthesized from a model of non-deterministic dynamic fault trees. The synthesis is performed by transforming non-deterministic dynamic fault trees into Markov automata that represent all possible choices between recovery actions. From the corresponding scheduler, optimized for maximum expected long-term reachability of failure states, a recovery strategy, optimal with respect to mean time to failure, can then be derived and represented by a model we call recovery automaton. We discuss techniques for reducing the state space of this recovery automaton, and analyze their soundness and completeness. We show that they do not generally guarantee recovery automata with the minimal number of states and derive a class where this guarantee holds. Implementation details for our approach are given and its effectiveness is verified on the basis of three case studies