Formalization of Fault Trees in Higher-Order Logic: A Deep Embedding Approach

  • Waqar AhmadEmail author
  • Osman Hasan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


Fault Tree (FT) is a standard failure modeling technique that has been extensively used to predict reliability, availability and safety of many complex engineering systems. In order to facilitate the formal analysis of FT based analyses, a higher-order-logic formalization of FTs has been recently proposed. However, this formalization is quite limited in terms of handling large systems and transformation of FT models into their corresponding Reliability Block Diagram (RBD) structures, i.e., a frequently used transformation in reliability and availability analyses. In order to overcome these limitations, we present a deep embedding based formalization of FTs. In particular, the paper presents a formalization of AND, OR and NOT FT gates, which are in turn used to formalize other commonly used FT gates, i.e., NAND, NOR, XOR, Inhibit, Comparator and majority Voting, and the formal verification of their failure probability expressions. For illustration purposes, we present a formal failure analysis of a communication gateway software for the next generation air traffic management system.


Higher-order logic Fault Tree Theorem proving 


  1. 1.
    ReliaSoft (2016).
  2. 2.
  3. 3.
    Trivedi, K.S.: Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley, New York (2002)zbMATHGoogle Scholar
  4. 4.
    Epstein, S., Rauzy, A.: Can we trust PRA? Reliab. Eng. Syst. Saf. 88(3), 195–205 (2005)CrossRefGoogle Scholar
  5. 5.
    Ahmed, 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, Heidelberg (2015). doi: 10.1007/978-3-319-20615-8_3 CrossRefGoogle Scholar
  6. 6.
    Bilintion, R., Allan, R.: Reliability Evaluation of Engineering Systems. Springer, New York (1992)CrossRefGoogle Scholar
  7. 7.
    Ahmed, W., Hasan, O., Tahar, S.: Formalization of reliability block diagrams in higher-order logic. J. Appl. Logic 18, 19–41 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173–186. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04468-7_15 CrossRefGoogle Scholar
  9. 9.
    Ortmeier, F., Schellhorn, G.: Formal fault tree analysis-practical experiences. Electron. Notes Theoret. Comput. Sci. 185, 139–151 (2007). ElsevierCrossRefzbMATHGoogle Scholar
  10. 10.
    Xiang, J., Futatsugi, K., He, Y.: Fault tree and formal methods in system safety analysis. In: IEEE Computer and Information Technology, pp. 1108–1115 (2004)Google Scholar
  11. 11.
    Futatsugi, K., Nakagawa, A.T., Tamai, T.: CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier, Elsevier (2000)Google Scholar
  12. 12.
    Mhamdi, T., Hasan, O., Tahar, S.: On the formalization of the Lebesgue integration theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 387–402. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14052-5_27 CrossRefGoogle Scholar
  13. 13.
    Ahmed, W., Hasan, O., Tahar, S., Hamdi, M.S.: Towards the formal reliability analysis of oil and gas pipelines. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 30–44. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-08434-3_4 Google Scholar
  14. 14.
    Ahmed, W., Hasan, O., Tahar, S.: Formal reliability analysis of wireless sensor network data transport protocols using HOL. In: IEEE Wireless and Mobile Computing, Networking and Communications, pp. 217–224 (2015)Google Scholar
  15. 15.
    Ahmad, W., Hasan, O., Tahar, S., Hamdi, M.: Towards formal reliability analysis of logistics service supply chains using theorem proving. In: Implementation of Logics, pp. 111–121 (2015)Google Scholar
  16. 16.
    Ahmed, W., Hasan, O.: Formal availability analysis using theorem proving. In: International Conference on Formal Engineering Methods. LNCS, pp. 1–16. Springer, Switzerland (2016, to appear). arXiv:1608.01755
  17. 17.
    Kuykendall, T.A.: Section 3.9, fault tree to RBD transformation. In: Systems Engineering “Toolbox” for Design-Oriented Engineers, pp. 52–52. NASA (1994)Google Scholar
  18. 18.
    Törngren, M.: Fundamentals of implementing real-time control applications in distributed computer systems. Real-Time Syst. 14(3), 219–250 (1998)CrossRefGoogle Scholar
  19. 19.
    Kornecki, A.J., Liu, M.: Fault tree analysis for safety/security verification in aviation software. Electronics 2(1), 41–56 (2013)CrossRefGoogle Scholar
  20. 20.
    Ahmad, W.: Formalization of fault trees in higher-order logic: a deep embedding approach (2016).

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.School of Electrical Engineering and Computer ScienceNational University of Sciences and TechnologyIslamabadPakistan

Personalised recommendations