Formal Fault Tree Analysis using a Hybrid Model Checking and Theorem Proving based Approach

Abstract: Fault Tree Analysis (FTA) is one of the most commonly used safety assessment tool to study the behavior of complex engineering systems in the presence of potential faults and the impact of malfunctioning sub-components on the overall system failure. Traditionally, FTA is performed analytically or using computer simulations. However, the former is prone to human error and the later does not provide a complete analysis, which makes them inappropriate for FTA of safety and security-critical systems. To overcome these limitations, we propose a hybrid model checking and theorem proving based formal verification based approach for FTA. The proposed approach utilizes the nuXmv model checker to develop and functionally verify the given system. The SMV model, used in the nuXmv model checker, is then utilized in the xSAP tool to extract the Fault Tree (FT) of the given system against a given property. This property definition based generated FT is then translated in higher-order logic to formally derive generic expressions regarding the probability of failure of the given system within the sound environment of the HOL4 theorem prover. For illustration, we utilized the proposed approach for analyzing a triple redundant generator system.

Code of TRG Circuit Taken from xSAP Manual: IEEE-SW-Code

HOL Code:HOL-FT-Code