Synthesizing FDIR recovery strategies for space systems

Müller, Sascha; Katoen, Joost-Pieter; Noll, Thomas; Gerndt, Andreas

doi:42362

Synthesizing FDIR recovery strategies for space systems

Müller, Sascha^RWTH*

2023

Verantwortlichkeitsangabevorgelegt von Sascha Müller

ImpressumAachen : RWTH Aachen University 2023

Umfang1 Online-Ressource : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2023

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Noll, Thomas (Thesis advisor)^RWTH* ; Gerndt, Andreas (Thesis advisor) ; Katoen, Joost-Pieter (Thesis advisor)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2023-01-12

Online
DOI: 10.18154/RWTH-2023-06510
URL: https://publications.rwth-aachen.de/record/960918/files/960918.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
FDIR (frei) ; Fehlerbaumanalyse (frei) ; Synthese (frei) ; Zuverlässigkeitstechnik (frei) ; fault tree analysis (frei) ; formal methods (frei) ; formale Methoden (frei) ; reliability engineering (frei) ; synthesis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Dynamic Fault Trees (DFTs) sind wirkungsvolle Werkzeuge um fehlertolerante Systeme zu designen. Allerdings limitieren semantische Fallstricke ihren praktischen Nutzen bei eng verknüpften Systemen, welche komplexe Wiederherstellungsstrategien benötigen um ihre Zuverlässigkeit zu maximieren. Diese Arbeit diskutiert die Schwächen von DFTs in dem Kontext von Fault Detection, Isolation and Recovery (FDIR) Konzeptanalysen mit einem Fokus auf Raumfahrtsystemen.Als Ansatz führen wir ein nicht-deterministisches DFT Modell ein. Durch eine Transformation in Markov-Automaten werden dann Wiederherstellungstrategien synthetisiert. Für die Synthese wird hierzu der optimale Scheduler ermittelt, welcher eine gegebene RAMS (Reliability, Availability, Maintainability and Safety) Metrik optimiert, und dieser dann in ein von uns Recovery Automat genanntes Modell weitertransformiert. Um den Zustandsraum des Recovery Automaten zu reduzieren, entwickeln wir dedizierte Techniken und analysieren diese auf ihre Korrektheit. Außerdem werden modulare Ansätze betrachtet um die Komplexitätszunahme durch den Zustandsraumbasierten Ansatz zu handhaben. Weiterhin untersuchen wir den nicht-deterministischen Ansatz in einem bedingt observierbaren Kontext. Für den vorgeschlagenen Ansatz diskutieren wir eine von uns angefertigte Implementierung innerhalb des Virtual Satellite Frameworks. Abschließend evaluieren wir die Implementierung mithilfe des FFORT Benchmarks. Die Ergebnisse zeigen, dass nicht-deterministische DFTs im Allgemeinen gut skalieren. Es lässt sich allerdings auch feststellen, dass semantisch erweiterte Versionen, welche zum Beispiel mit Reparaturmechanismen oder bedingter Observierbarkeit ausgestattet sind, eine Herausforderung darstellen.

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.

OpenAccess:
PDF
(additional files)