Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking

被引:7
作者
Elderhalli, Yassmeen [1 ]
Hasan, Osman [1 ]
Ahmad, Waqar [1 ]
Tahar, Sofiene [1 ]
机构
[1] Concordia Univ, Elect & Comp Engn, Montreal, PQ, Canada
来源
NASA FORMAL METHODS, NFM 2018 | 2018年 / 10811卷
关键词
Dynamic fault trees; Theorem proving; Model checking; HOL4; STORM;
D O I
10.1007/978-3-319-77935-5_10
中图分类号
V [航空、航天];
学科分类号
08 ; 0825 ;
摘要
Dynamic fault trees (DFTs) have emerged as an important tool for capturing the dynamic behavior of system failure. These DFTs are analyzed qualitatively and quantitatively using stochastic or algebraic methods. Model checking has been proposed to conduct the failure analysis of systems using DFTs. However, it has not been used for DFT qualitative analysis. Moreover, its analysis time grows exponentially with the number of states and its reduction algorithms are usually not formally verified. To overcome these limitations, we propose a methodology to perform the formal analysis of DFTs using an integration of theorem proving and model checking. We formalize the DFT gates in higher-order logic and formally verify many algebraic simplification properties using theorem proving. Based on this, we prove the equivalence between raw DFTs and their reduced forms to enable the formal qualitative analysis (determine the cut sets and sequences) of DFTs with theorem proving. We then use model checking to perform the quantitative analysis (compute probabilities of failure) of the formally verified reduced DFT. We applied our methodology on five benchmarks and the results show that the formally verified reduced DFT was analyzed using model checking with up to six times less states and up to 133000 times faster.
引用
收藏
页码:139 / 156
页数:18
相关论文
共 16 条
  • [1] Formalization of Fault Trees in Higher-Order Logic: A Deep Embedding Approach
    Ahmed, Waqar
    Hasan, Osman
    [J]. DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, 2016, 9984 : 264 - 279
  • [2] Towards Formal Fault Tree Analysis Using Theorem Proving
    Ahmed, Waqar
    Hasan, Osman
    [J]. INTELLIGENT COMPUTER MATHEMATICS, CICM 2015, 2015, 9150 : 39 - 54
  • [3] [Anonymous], 2002, FAULT TREE HDB AEROS
  • [4] [Anonymous], 2010, THESIS
  • [5] Arnold Florian, 2013, Computer Safety, Reliability and Security. 32nd International Conference, SAFECOMP 2013. Proceedings: LNCS 8153, P293, DOI 10.1007/978-3-642-40793-2_27
  • [6] A new Bayesian network approach to solve dynamic fault trees
    Boudali, H
    Dugan, JB
    [J]. ANNUAL RELIABILITY AND MAINTAINABILITY SYMPOSIUM, 2005 PROCEEDINGS, 2005, : 451 - 456
  • [7] Boudali H, 2007, LECT NOTES COMPUT SC, V4762, P441
  • [8] A STORM is Coming: A Modern Probabilistic Model Checker
    Dehnert, Christian
    Junges, Sebastian
    Katoen, Joost-Pieter
    Volk, Matthias
    [J]. COMPUTER AIDED VERIFICATION (CAV 2017), PT II, 2017, 10427 : 592 - 600
  • [9] Elderhalli Y., 2017, TECHNICAL REPORT
  • [10] Elderhalli Y., 2017, DFT FORMAL ANAL HOL4