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

Abstract

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.

Authors 3

1. Shahid Ali Khan Aachen Software Modeling and Verification

   RWTH Aachen University · National University of Sciences and Technology

   Affiliation as printed

   National University of Sciences and Technology (NUST),Sch. of Elect. Engg. and Computer Sc.,Islamabad,Pakistan

   Sch. of Elect. Engg. and Computer Sc., National University of Sciences and Technology (NUST), Islamabad, Pakistan

   Software Modeling and Verification, RWTH Aachen University, Aachen, Germany

2. Waqar Ahmad

   National University of Sciences and Technology

   Affiliation as printed

   National University of Sciences and Technology (NUST),Sch. of Elect. Engg. and Computer Sc.,Islamabad,Pakistan

   Sch. of Elect. Engg. and Computer Sc., National University of Sciences and Technology (NUST), Islamabad, Pakistan

3. Osman Hasan

   National University of Sciences and Technology

   Affiliation as printed

   National University of Sciences and Technology (NUST),Sch. of Elect. Engg. and Computer Sc.,Islamabad,Pakistan

   Sch. of Elect. Engg. and Computer Sc., National University of Sciences and Technology (NUST), Islamabad, Pakistan