Skip to main content

2016 | OriginalPaper | Buchkapitel

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

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
3.
Zurück zum Zitat Trivedi, K.S.: Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley, New York (2002)MATH Trivedi, K.S.: Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley, New York (2002)MATH
4.
Zurück zum Zitat Epstein, S., Rauzy, A.: Can we trust PRA? Reliab. Eng. Syst. Saf. 88(3), 195–205 (2005)CrossRef Epstein, S., Rauzy, A.: Can we trust PRA? Reliab. Eng. Syst. Saf. 88(3), 195–205 (2005)CrossRef
5.
Zurück zum Zitat 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 CrossRef 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 CrossRef
6.
Zurück zum Zitat Bilintion, R., Allan, R.: Reliability Evaluation of Engineering Systems. Springer, New York (1992)CrossRef Bilintion, R., Allan, R.: Reliability Evaluation of Engineering Systems. Springer, New York (1992)CrossRef
7.
Zurück zum Zitat Ahmed, W., Hasan, O., Tahar, S.: Formalization of reliability block diagrams in higher-order logic. J. Appl. Logic 18, 19–41 (2016)MathSciNetCrossRefMATH Ahmed, W., Hasan, O., Tahar, S.: Formalization of reliability block diagrams in higher-order logic. J. Appl. Logic 18, 19–41 (2016)MathSciNetCrossRefMATH
8.
Zurück zum Zitat 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 CrossRef 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 CrossRef
9.
Zurück zum Zitat Ortmeier, F., Schellhorn, G.: Formal fault tree analysis-practical experiences. Electron. Notes Theoret. Comput. Sci. 185, 139–151 (2007). ElsevierCrossRefMATH Ortmeier, F., Schellhorn, G.: Formal fault tree analysis-practical experiences. Electron. Notes Theoret. Comput. Sci. 185, 139–151 (2007). ElsevierCrossRefMATH
10.
Zurück zum Zitat 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) 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)
11.
Zurück zum Zitat Futatsugi, K., Nakagawa, A.T., Tamai, T.: CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier, Elsevier (2000) Futatsugi, K., Nakagawa, A.T., Tamai, T.: CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier, Elsevier (2000)
12.
Zurück zum Zitat 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 CrossRef 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 CrossRef
13.
Zurück zum Zitat 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 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
14.
Zurück zum Zitat 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) 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)
15.
Zurück zum Zitat 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) 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)
16.
Zurück zum Zitat 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 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.
Zurück zum Zitat Kuykendall, T.A.: Section 3.9, fault tree to RBD transformation. In: Systems Engineering “Toolbox” for Design-Oriented Engineers, pp. 52–52. NASA (1994) Kuykendall, T.A.: Section 3.9, fault tree to RBD transformation. In: Systems Engineering “Toolbox” for Design-Oriented Engineers, pp. 52–52. NASA (1994)
18.
Zurück zum Zitat Törngren, M.: Fundamentals of implementing real-time control applications in distributed computer systems. Real-Time Syst. 14(3), 219–250 (1998)CrossRef Törngren, M.: Fundamentals of implementing real-time control applications in distributed computer systems. Real-Time Syst. 14(3), 219–250 (1998)CrossRef
19.
Zurück zum Zitat Kornecki, A.J., Liu, M.: Fault tree analysis for safety/security verification in aviation software. Electronics 2(1), 41–56 (2013)CrossRef Kornecki, A.J., Liu, M.: Fault tree analysis for safety/security verification in aviation software. Electronics 2(1), 41–56 (2013)CrossRef
Metadaten
Titel
Formalization of Fault Trees in Higher-Order Logic: A Deep Embedding Approach
verfasst von
Waqar Ahmad
Osman Hasan
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-47677-3_17