Fault Tree Analysis of Safety-Critical Systems via Statistical Model Checking

The design of safety-critical systems have become more and more complex in recent years. As a result, identifying the sources of failure and mitigating their effects on the system are of great importance. In this context, several methods have been proposed. One of the widely-used approaches for reliability analysis of systems is fault tree analysis (FTA). The traditional methods of FTA that are based on paper and pencil proof or simulation can be drastically time-consuming and highly prone to error, especially when analyzing complex systems with redundant architectures. In this work, we propose a statistical model checking (SMC) based approach for FTA of safety critical systems that can mitigate the above-mentioned problems regarding the traditional FTA methods. In our approach, the FT gates are modelled using the priced timed automata (PTA) formalism, and then the full fault tree model is created by the parallel composition of the models of each gate. Furthermore, in our method, the FT models take into account both the power consumption and failure rates of the system components. With this, it becomes possible to determine when the power source will run out of power and then the mission time of the system can be determined. As a result, the FTA time period can be restricted to the system’s mission time and the resources can be used more efficiently. Our proposed approach is also able to perform a formal assessment of the FT model. This evaluation includes a criticality analysis to identify the fault tree’s critical elements that have the greatest impact on the probability of system failure. The critical FT components are then subjected to various risk mitigation techniques based on component redundancy, such as triple modular redundancy (TMR) and quintuple modular redundancy (QMR)