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)
Doktorarbeit

Dissertation, RWTH Aachen University, 2023

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.

Einrichtungen

• Fachgruppe Informatik [120000]
• Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) [121310]