SAFEST: Fault Tree Analysis Via Probabilistic Model Checking

This paper presents SAFEST, a powerful tool for modelling and analyzing both static and dynamic fault trees. Dynamic fault trees (DFTs) extend standard fault trees by providing support for faithfully modelling spare management, functional dependencies, and order-dependent failures. The SAFEST tool provides efficient and powerful analysis of DFTs via probabilistic model checking - a rigorous, automated analysis technique for probabilistic systems. The backbone of the analysis is based on efficient state space generation. Several optimization techniques are incorporated, such as exploiting irrelevant failures, symmetries, and independent modules. Probabilistic model checking allows to analyze the resulting state space with respect to a wide range of measures of interest. In addition, an approximation approach is provided that builds only parts of the state space and allows to iteratively refine the computations up to the desired accuracy. The SAFEST tool provides a graphical user interface for creating, generating, simulating, and simplifying fault trees as well as visualizing the results from the fault tree analysis. SAFEST is state of the art for DFT analysis, as demonstrated by an experimental evaluation and comparison with existing tools. In addition, SAFEST and DFT models have been applied in a variety of case studies, including vehicle guidance systems, train operations in railway station areas, and energy systems such as (nuclear) power plants.