Dynamic fault trees: semantics, analysis and applications

Volk, Matthias; Cimatti, Alessandro; Katoen, Joost-Pieter

doi:HT021880200

Dynamic fault trees: semantics, analysis and applications

Volk, Matthias^RWTH*

2022 & 2023

Verantwortlichkeitsangabevorgelegt von Matthias Volk, M. Sc.

ImpressumAachen : RWTH Aachen University 2022

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2022

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2023

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Cimatti, Alessandro (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2022-04-28

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

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
dynamic fault trees (frei) ; fault tree analysis (frei) ; formal methods (frei) ; probabilistic model checking (frei) ; reliability (frei) ; safety (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Sichere und zuverlässige Systeme sind von entscheidender Bedeutung in der heutigen Zeit. Ausfälle können schwerwiegende Folgen haben und reichen von Leistungseinbußen über ökologische und wirtschaftliche Schäden bis hin zum Verlust von Menschenleben. Die wachsende Anzahl von Systemen, die Zunahme von cyber-physischen Systemen und die breite Vernetzung von Komponenten führen zu einer immer größer werdenden Komplexität. Eine Vielzahl von Ansätzen und formalen Modellen ist vorgeschlagen worden, um die Zuverlässigkeit von Systemen zu analysieren und zu verbessern. Fehlerbäume sind ein bekanntes und weit verbreitetes Modell in der Zuverlässigkeitsanalyse. Fehlerbäume modellieren, wie sich Ausfälle von Komponenten in einem System ausbreiten und zu einem Ausfall des Gesamtsystems führen. Während Fehlerbäume in der Industrie weit verbreitet sind, berücksichtigt ihre statische Natur nicht das dynamische Verhalten, welches in modernen Systemen vorhanden ist. Dynamische Fehlerbäume (DFTs) sind eine Erweiterung von statischen Fehlerbäumen und ermöglichen mehr Flexibilität in der Modellierung durch die Einführung von dynamischen Gattern, Management von Reserveteilen, funktionalen Abhängigkeiten und Einschränkungen von Ausfällen. In dieser Arbeit untersuchen wir dynamische Fehlerbäume im Detail und betrachten drei Hauptaspekte: (1) die prä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 Fehlerbäumen. Wir präsentieren eine präzise Definition der Semantik fü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 für DFTs vor. Unsere Analyse basiert auf Model-Checking für probabilistische Systeme und verwendet Markov-Automaten als Basis-Modell. Die Analyse nutzt effiziente Standard-Algorithmen für das Model-Checking und ermöglicht es, eine breite Auswahl von Metriken zu berechnen, die weit über die typischerweise berechnete Zuverlässigkeit hinausgehen. Wir stellen mehrere (orthogonale) Optimierungen vor, die unter anderem Symmetrien, irrelevante Ausfälle und unabhängige Teilbäume ausnutzen, um die Generierung des Zustandsraums zu beschleunigen. Zusätzlich entwickeln wir einen Approximationsalgorithmus, der nur Teile des Zustandsraums generiert. Der Zustandsraum wird dabei solange iterativ verfeinert, bis die gewünschte Genauigkeit des Ergebnisses erreicht ist. Alle vorgestellten Ansä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 für die DFT-Analyse ist. Im dritten Teil präsentieren wir den Einsatz von DFTs im (1) Automobil- und (2) Eisenbahnbereich. Die erste Fallstudie betrachtet ein Fahrzeugführungssystem für autonomes Fahren. Wir modellieren verschiedene Sicherheitskonzepte und analysieren verschiedene Zuordnungen von Funktionen auf die Hardware. Die resultierenden Modelle gehören zu den bisher größten analysierten DFTs. Die zweite Fallstudie betrachtet die Zugführung in Bahnhofsbereichen unter Berücksichtigung der verfügbaren Infrastrukturelemente. Die DFTs werden automatisch aus den gegebenen Infrastrukturdaten und Trasseninformationen generiert. Wir analysieren, wie sich Weichenausfälle auf die möglichen Zugrouten in einem Bahnhof auswirken und ermitteln die kritischsten Komponenten.

Safe and reliable systems are crucial in today’s society. Failures can have severe consequences, ranging from performance degradation over environmental and economic costs to loss of human lives. The growing number of systems, the rise of cyber-physical systems and the connectedness of components lead to an ever increasing complexity. A broad range of approaches and formal models have been proposed to analyse and improve the reliability of systems. Fault trees are a prominent and widely-used model in reliability engineering. They model how component failures propagate through a system and lead to a failure of the overall system. While fault trees are widely adopted in industry, their static nature discards dynamic behaviour present in modern systems. Dynamic fault trees (DFTs) are an extension of static fault trees and allow more modelling flexibility by introducing dynamic gates, spare management, functional dependencies and failure restrictions. In this thesis, we investigate dynamic fault trees in detail and consider three main aspects: (1) the precise semantics of DFTs, (2) the analysis of DFTs by model checking techniques, and (3) the application of DFTs in the automotive and railway domain. In the first part we specify the semantics of dynamic fault trees. We present a precise definition of the semantics for each DFT element in terms of generalized stochastic Petri nets (GSPNs). We also investigate multiple semantic questions resulting from the combination of DFT elements. Our resulting framework based on GSPNs subsumes the major existing DFT semantics and allows to pinpoint their differences. The second part presents analysis techniques for DFTs. Our analysis is based on probabilistic model checking and uses Markov automata as the underlying model. The analysis exploits efficient, off-the-shelf algorithms for model checking and allows to compute a broad range of measures which go far beyond typical reliability. We present several (orthogonal) optimisation techniques which exploit symmetries, irrelevant failures and independent subtrees to improve the state-space generation times. Additionally, we develop an approximation algorithm based on partial state-space exploration which iteratively refines the state space until the desired precision of the result is reached. All presented approaches are implemented in the open-source model checker Storm and are evaluated on a DFT benchmark suite. The evaluation shows that our tool Storm-dft is state-of-the-art for DFT analysis. The third part presents the application of DFTs in both (1) the automotive and (2) railway domain. The first case study considers a vehicle guidance system for autonomous driving. We model several safety concepts and analyse different partitionings of functions on hardware. The resulting models are among the largest DFTs to date. The second case study considers train routing options in railway station areas in terms of available infrastructure elements. The DFTs are automatically generated from the given infrastructure data and train path information. We analyse how switch failures impact the potential train routes in a station and determine the most critical components.

OpenAccess:
PDF
(additional files)