Synthesizing FDIR recovery strategies for space systems

Müller, Sascha; Noll, Thomas (Thesis advisor); Gerndt, Andreas (Thesis advisor); Katoen, Joost-Pieter (Thesis advisor)

Aachen : RWTH Aachen University (2023)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2023


Dynamic Fault Trees (DFTs) are powerful tools to drive the design of fault-tolerant systems. However, semantic pitfalls limit their practical utility for interconnected systems that require complex recovery strategies to maximize their reliability. This thesis discusses the shortcomings of DFTs in the context of analyzing Fault Detection, Isolation and Recovery (FDIR) concepts with a particular focus on the needs of space systems. To tackle these shortcomings, we introduce an inherently non-deterministic model for DFTs. Deterministic recovery strategies are synthesized by transforming these non-deterministic DFTs into Markov automata that represent all possible choices between recovery actions. From the corresponding scheduler, optimized to maximize a given RAMS (Reliability, Availability, Maintainability and Safety) metric, an optimal recovery strategy can then be derived and represented by a model we call recovery automaton. We discuss dedicated techniques for reducing the state space of this recovery automaton and analyze their soundness and completeness. Moreover, modularized approaches to handle the complexity added by the state-based transformation approach are discussed. Furthermore, we consider the non-deterministic approach in a partially observable setting and propose an approach to lift the model for the fully observable case. We give an implementation of our approach within the Model-Based Systems Engineering (MBSE) framework Virtual Satellite. Finally, the implementation is evaluated based on the FFORT benchmark. The results show that basic non-deterministic DFTs generally scale well. However, we also found that semantically enriched non-deterministic DFTs employing repair or delayed observability mechanisms pose a challenge.


  • Department of Computer Science [120000]
  • Chair of Computer Science 2 (Software Modeling and Verification) [121310]