Dynamic fault trees: semantics, analysis and applications

Volk, Matthias; Katoen, Joost-Pieter (Thesis advisor); Cimatti, Alessandro (Thesis advisor)

Aachen : RWTH Aachen University (2022, 2023)
Doktorarbeit

Dissertation, RWTH Aachen University, 2022

Kurzfassung

Sichere und zuverlässige Systeme sind von entscheidender Bedeutung in der heutigen Zeit. Ausfälle können schwerwiegende Folgen haben und reichen von Leistungseinbußen über ökologische und wirtschaftliche Schäden bis hin zum Verlust von Menschenleben. Die wachsende Anzahl von Systemen, die Zunahme von cyber-physischen Systemen und die breite Vernetzung von Komponenten führen zu einer immer größer werdenden Komplexität. Eine Vielzahl von Ansätzen und formalen Modellen ist vorgeschlagen worden, um die Zuverlässigkeit von Systemen zu analysieren und zu verbessern. Fehlerbäume sind ein bekanntes und weit verbreitetes Modell in der Zuverlässigkeitsanalyse. Fehlerbäume modellieren, wie sich Ausfälle von Komponenten in einem System ausbreiten und zu einem Ausfall des Gesamtsystems führen. Während Fehlerbäume in der Industrie weit verbreitet sind, berücksichtigt ihre statische Natur nicht das dynamische Verhalten, welches in modernen Systemen vorhanden ist. Dynamische Fehlerbäume (DFTs) sind eine Erweiterung von statischen Fehlerbäumen und ermöglichen mehr Flexibilität in der Modellierung durch die Einführung von dynamischen Gattern, Management von Reserveteilen, funktionalen Abhängigkeiten und Einschränkungen von Ausfällen. In dieser Arbeit untersuchen wir dynamische Fehlerbäume im Detail und betrachten drei Hauptaspekte: (1) die präzise Semantik von DFTs, (2) die Analyse von DFTs mit Hilfe von Model-Checking-Techniken und (3) den Einsatz von DFTs im Automobil- und Eisenbahnbereich. Im ersten Teil spezifizieren wir die Semantik von dynamischen Fehlerbäumen. Wir präsentieren eine präzise Definition der Semantik für jedes DFT-Element in Form von generalisierten stochastischen Petri-Netzen (GSPNs). Außerdem untersuchen wir mehrere semantische Fragestellungen, die sich aus der Kombination von verschiedenen DFT-Elementen ergeben. Unser Modell auf Basis von GSPNs umfasst die wichtigsten existierenden DFT-Semantiken und erlaubt es, ihre Unterschiede genau zu bestimmen. Der zweite Teil stellt Analysetechniken für DFTs vor. Unsere Analyse basiert auf Model-Checking für probabilistische Systeme und verwendet Markov-Automaten als Basis-Modell. Die Analyse nutzt effiziente Standard-Algorithmen für das Model-Checking und ermöglicht es, eine breite Auswahl von Metriken zu berechnen, die weit über die typischerweise berechnete Zuverlässigkeit hinausgehen. Wir stellen mehrere (orthogonale) Optimierungen vor, die unter anderem Symmetrien, irrelevante Ausfälle und unabhängige Teilbäume ausnutzen, um die Generierung des Zustandsraums zu beschleunigen. Zusätzlich entwickeln wir einen Approximationsalgorithmus, der nur Teile des Zustandsraums generiert. Der Zustandsraum wird dabei solange iterativ verfeinert, bis die gewünschte Genauigkeit des Ergebnisses erreicht ist. Alle vorgestellten Ansätze werden in dem Open-Source-Tool Storm implementiert und auf einer Sammlung von DFT-Beispielen evaluiert. Die Evaluierung zeigt, dass unser Tool Storm-dft der aktuelle Stand der Technik für die DFT-Analyse ist. Im dritten Teil präsentieren wir den Einsatz von DFTs im (1) Automobil- und (2) Eisenbahnbereich. Die erste Fallstudie betrachtet ein Fahrzeugführungssystem für autonomes Fahren. Wir modellieren verschiedene Sicherheitskonzepte und analysieren verschiedene Zuordnungen von Funktionen auf die Hardware. Die resultierenden Modelle gehören zu den bisher größten analysierten DFTs. Die zweite Fallstudie betrachtet die Zugführung in Bahnhofsbereichen unter Berücksichtigung der verfügbaren Infrastrukturelemente. Die DFTs werden automatisch aus den gegebenen Infrastrukturdaten und Trasseninformationen generiert. Wir analysieren, wie sich Weichenausfälle auf die möglichen Zugrouten in einem Bahnhof auswirken und ermitteln die kritischsten Komponenten.

Einrichtungen

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