A Hybrid Model Checking and Theorem Proving based Approach for Fault Tree Analysis

Static fault trees (SFT)s are used for conducting dependability analysis and thus are extensively utilized in various functional safety standards defined by the IEC and ISO for automotive applications. Traditionally, SFTs are manually developed by domain experts through a very cumbersome and error prone process. Once the SFT is available, quantitative fault tree analysis (FTA) is carried out using analytical approaches, e.g., probabilistic model checking and theorem proving. While the former is limited to exponential distributions, the latter can analyze fault trees (FT)s with arbitrary probability distributions. This paper proposes to combine model checking-based automatic FT generation and theorem proving based FTA to ensure a more rigorous and complete approach for FTA. The proposed approach particularly utilizes 1) the xSAP safety assessment platform to automatically generate SFTs from a functionally verified system model and 2) the HOL4 theorem prover to analyze the xSAP-generated SFTs. The usefulness of the approach is illustrated using the case study of an automated vehicle system.