Advertisement

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

  • Yassmeen Elderhalli
  • Osman Hasan
  • Waqar Ahmad
  • Sofiène Tahar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)

Abstract

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.

Keywords

Dynamic fault trees Theorem proving Model checking HOL4 STORM 

References

  1. 1.
    Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15–16, 29–62 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Stamatelatos, M., Vesely, W., Dugan, J., Fragola, J., Minarick, J., Railsback, J.: Fault tree handbook with aerospace applications. NASA Office of Safety and Mission Assurance (2002)Google Scholar
  3. 3.
    Merle, G.: Algebraic Modelling of Dynamic Fault Trees, Contribution to Qualitative and Quantitative Analysis. Ph.D. thesis, ENS, France (2010)Google Scholar
  4. 4.
    Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_31 CrossRefGoogle Scholar
  5. 5.
    Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Inf. 14, 370–379 (2017).  https://doi.org/10.1109/TII.2017.2710316 CrossRefGoogle Scholar
  6. 6.
    Ahmad, W., Hasan, O.: Towards formal fault tree analysis using theorem proving. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 39–54. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-20615-8_3 CrossRefGoogle Scholar
  7. 7.
    Boudali, H., Crouzen, P., Stoelinga, M.: A compositional semantics for dynamic fault trees in terms of interactive Markov chains. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 441–456. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-75596-8_31 CrossRefGoogle Scholar
  8. 8.
    Merle, G., Roussel, J.M., Lesage, J.J., Bobbio, A.: Probabilistic algebraic analysis of fault trees with priority dynamic gates and repeated events. IEEE Trans. Reliab. 59(1), 250–261 (2010)CrossRefGoogle Scholar
  9. 9.
    Malhotra, M., Trivedi, K.S.: Dependability modeling using petri-nets. IEEE Trans. Reliab. 44(3), 428–440 (1995)CrossRefGoogle Scholar
  10. 10.
    Boudali, H., Dugan, J.: A new Bayesian network approach to solve dynamic fault trees. In: IEEE Reliability and Maintainability Symposium, pp. 451–456 (2005)Google Scholar
  11. 11.
    HOL4 (2017). hol.sourceforge.net
  12. 12.
    Pullum, L., Dugan, J.: Fault tree models for the analysis of complex computer-based systems. In: IEEE Reliability and Maintainability Symposium, pp. 200–207 (1996)Google Scholar
  13. 13.
  14. 14.
    Arnold, F., Belinfante, A., Van der Berg, F., Guck, D., Stoelinga, M.: DFTCalc: a tool for efficient fault tree analysis. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 293–301. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40793-2_27 CrossRefGoogle Scholar
  15. 15.
    Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., Volk, M.: Model-based safety analysis for vehicle guidance systems. In: Tonetta, S., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2017. LNCS, vol. 10488, pp. 3–19. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66266-4_1 CrossRefGoogle Scholar
  16. 16.
    Ahmad, W., Hasan, O.: Formalization of fault trees in higher-order logic: a deep embedding approach. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 264–279. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47677-3_17 CrossRefGoogle Scholar
  17. 17.
    Elderhalli, Y.: DFT Formal Analysis: HOL4 Script and Storm Benchmarks (2017). http://hvg.ece.concordia.ca/Publications/TECH_REP/DFT_TR17
  18. 18.
    Elderhalli, Y., Hasan, O., Ahmad, W., Tahar, S.: Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking. Technical report, Concordia University, Canada (2017). https://arxiv.org/abs/1712.02872

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Electrical and Computer EngineeringConcordia UniversityMontréalCanada

Personalised recommendations