Dynamic fault trees: semantics, analysis and applications

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

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

Dissertation, RWTH Aachen University, 2022

Abstract

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.

Institutions

• UnRAVeL Research Training Group [080060]
• Department of Computer Science [120000]
• Chair of Computer Science 2 (Software Modeling and Verification) [121310]