Verifying Fault Trees for Railway Safety
Fault trees (FTs) are a key technique in safety and reliability engineering. Their analysis is one of the most prominent safety assessment techniques and recommended by standards in e.g. aerospace, nuclear power and automotive industries. Fault trees describe top-down causes for a system failure and model how component failures – represented in the leaves – lead to system failures. The failure propagation through the system is modelled by logical gates such as AND and OR.
As an example consider the fault tree given in [sft_example]. It models a simple level crossing for a railway track. The level crossing fails if either the controller stops working or both the motor and the spare motor fail.
Fault tree analysis can be performed using various efficient techniques. However, standard fault trees lack expressive power to model many aspects of realistic systems, e.g. spare management or dependencies. Dynamic fault trees (DFTs) as an extension of standard fault trees were introduced to overcome these limitations. DFTs introduce several new types of gates such as spares, functional dependencies and sequencing, and allow for a more faithful model. Their behaviour is described by continuous-time Markov chains (CTMCs).
An example of a DFT is given in [dft_example] which again models a level crossing. Using the additional SPARE gate it is now possible to faithfully model the spare management of the motor and the spare motor. As long as the primary motor is used, the spare motor is in a passive mode, leading to a reduced failure rate. Only if the primary motor fails, the spare motor is used and activated. Additionally, the priority AND (PAND) gate models the behaviour of the switch. If the motor fails while the switch is operational, the system switches to the spare motor. However, if the switch fails before the motor it is not possible to switch to the spare motor anymore and the system is considered failed already.
Dynamic fault tree analysis is a well-developed field in reliability engineering. However, the main bottleneck is the efficient generation and analysis of CTMCs. Our research showed that the state-space generation can be significantly boosted by exploiting reduction techniques from model checking, such as symmetry and partial-order reduction. Accompanied with a fast analysis of CTMCs using probabilistic model-checking algorithms, this yields a speed up by a few orders of magnitude compared to state-of- the-art techniques for DFTs.
The main objective of this doctoral research project is to apply and adapt these new technologies to the safety analysis of railway systems. We want to model railway infrastructure, e.g., train paths within a train station, as DFTs and analyse – among others – the reliability and performance implications of these infrastructure elements under the occurrences of failures. We aim to further improve existing state space generation techniques and develop new analysis approaches for DFTs to facilitate a faster and more thorough fault tree analysis by also taking into the account the context of railway engineering.
Possible research collaborations within the RTG exist in particular to the topic of parametric Markov chains. In a DFT, it might not be possible to specify the exact failure rates of all considered components. In that case, some failure rates could be left open by using parameters instead. Parametric Markov chain analysis then could synthesise acceptable failure rates for these components which still guarantee that the given safety requirements are satisfied.