An optimized method for generating fault tree from a counter-example
Qianxin Wei, Jian Jiao, Jiping Fan, Tingdi Zhao · 2016
With the development of the Model Based Systems Engineering (MBSE), the Model-based safety analysis (MBSA) process and techniques have been widely studied and applied, which include system modeling, safety properties verification and safety analysis. As a core task, model checking explores the state space of the system model to generate counter-examples which describe system state sequences not meeting safety requirements. Although these sequences are useful for safety analysis, we still need to get the traditional safety artifacts such as a fault tree to keep the conclusion complete. Many studies have focused on how to generate fault trees from the counter-example automatically. However, there are some disadvantages in the existing generation methods. For instance, the generated fault tree contains many branch redundancies making the respective tree broad and difficult to understand, which limits the effectiveness and efficiency of the model checking technique. Based on investigating model checking mechanisms and counter-example forms, and combined with the traditional fault tree algorithm, this paper proposed a new optimized method that can translate the system state sequence obtained from the counter-example in NuSMV into a fault tree. By analyzing system operation process and function flow, and considering system hierarchical decomposition as well, the structure of the generated fault tree can be optimized, including redundant nodes removing and dimensions reducing, to improve its logical hierarchy and readability. Finally, a case study about airborne equipment is provided to demonstrate and validate the proposed method.