Abstract
It is indispensable to identify an occurrence and a possible consequence of any undesirable events in different components/sub-systems of safety-critical systems, such as nuclear power plants and smart power grids that may often lead to a catastrophic accident and thus may result into financial losses and severe injuries. This process requires assessing the probabilities of occurrence of these events and is widely known as Probabilistic Risk Assessment (PRA). The frequently used methods for conducting the PRA are Event Tree Analysis (ETA), Functional Block Diagrams (FBD) and Cause Consequence Diagrams (CCD) (using Fault Trees (FT) and Reliability Block Diagrams (RBD)). We propose to use higher-Order-Logic (HOL) theorem proving for performing the formal PRA of safety-critical systems. In this paper, we present recent developments towards this direction and a roadmap towards a successful development of a framework for formal reasoning support for ETs, FBDs and CCDs in a HOL theorem prover.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
The HOL4 code for the ET formalization can be found at https://github.com/hvg-concordia/ET.
- 3.
The HOL4 code for the FBD formalization can be found at https://github.com/hvg-concordia/FBD.
- 4.
The HOL4 code for the FT-based CCD formalization can be found at https://github.com/hvg-concordia/CCD.
- 5.
The HOL4 code for the RBD-based CCD formalization can be found at https://github.com/hvg-concordia/CCD_RBD.
References
Abdelghany, M., Ahmad, W., Tahar, S.: Event tree reliability analysis of electrical power generation network using formal techniques. In: Electric Power and Energy Conference, pp. 1–7. IEEE (2020)
Abdelghany, M., Ahmad, W., Tahar, S.: Event tree reliability analysis of safety-critical systems using theorem proving. IEEE Syst. J. 16(2), 2899–2910 (2021)
Abdelghany, M., Ahmad, W., Tahar, S., Nethula, S.: ETMA: an efficient tool for event trees modeling and analysis. In: International Systems Conference, pp. 1–8. IEEE (2020)
Abdelghany, M., Tahar, S.: Cause-consequence diagram reliability analysis using formal techniques with application to electrical power networks. IEEE Access 9, 23929–23943 (2021)
Abdelghany, M., Tahar, S.: Formalization of RBD-based cause consequence analysis in HOL. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) CICM 2021. LNCS (LNAI), vol. 12833, pp. 47–64. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81097-9_4
Abdelghany, M., Tahar, S.: Formal probabilistic risk assessment of a nuclear power plant. In: Formal Techniques for Safety-Critical Systems, pp. 80–87 (2022)
Abdelghany, M., Tahar, S.: Formalization of functional block diagrams using HOL theorem proving. In: Lima, L., Molnár, V. (eds.) SBMF 2022. LNCS, vol. 13768, pp. 22–35. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-22476-8_2
Abdelghany, M., Tahar, S.: Reliability analysis of smart grids using formal methods. In: Fathi, M., Zio, E., Pardalos, P.M. (eds.) Handbook of Smart Energy Systems, pp. 147–163. Springer, Cham (2023). https://doi.org/10.1007/978-3-030-97940-9_81
Abdelghany, M.W.E.: Formal probabilistic risk assessment using theorem proving with applications in power systems. Ph.D. thesis, Concordia University, Montreal, QC, Canada (2021)
Ahmad, W.: Formal dependability analysis using higher-order-logic theorem proving. Ph.D. thesis, National University of Sciences & Technology, Islamabad, Pakistan (2017)
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, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_3
Ahmed, W., Hasan, O., Tahar, S.: Formalization of reliability block diagrams in higher-order logic. J. Appl. Log. 18, 19–41 (2016)
Andrews, J.D., Ridley, L.M.: Application of the cause-consequence diagram method to static systems. Reliab. Eng. Syst. Saf. 75(1), 47–58 (2002)
Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 54–56. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0058022
Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35746-6_1
Elderhalli, Y.: Dynamic dependability analysis using HOL theorem proving with application in multiprocessor systems. Ph.D. thesis, Concordia University, Montreal, QC, Canada (2019)
Elderhalli, Y., Ahmad, W., Hasan, O., Tahar, S.: Probabilistic analysis of dynamic fault trees using HOL theorem proving. J. Appl. Logics—IfCoLog J. Logics Appl. 6(3) (2019)
Elderhalli, Y., Hasan, O., Tahar, S.: A formally verified algebraic approach for dynamic reliability block diagrams. In: Ait-Ameur, Y., Qin, S. (eds.) ICFEM 2019. LNCS, vol. 11852, pp. 253–269. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32409-4_16
Elderhalli, Y., Hasan, O., Tahar, S.: A framework for formal dynamic dependability analysis using HOL theorem proving. In: Benzmüller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 105–122. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53518-6_7
Gardoni, P.: Risk and Reliability Analysis. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52425-2
Haimes, Y.Y.: Risk Modeling, Assessment, and Management. Wiley, Hoboken (2005)
Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Computational Logic, vol. 9, pp. 135–214 (2014)
Hasan, O., Tahar, S.: Formal verification methods. In: Encyclopedia of Information Science and Technology, 3rd edn, pp. 7162–7170. IGI Global (2015)
Hixenbaugh, A.: Fault Tree for Safety. Seattle: The Boeing Company, D6 53604 (1968)
Hutchins, G.: ISO \(31000\): \(2018\) Enterprise Risk Management. Greg Hutchins (2018)
Kumamoto, H.: Satisfying Safety Goals by Probabilistic Risk Assessment. Springer, London (2007). https://doi.org/10.1007/978-1-84628-682-7
Leitch, M.: ISO \(31000\): \(2009\)-the new international standard on risk management. Risk Anal. 30(6), 887 (2010)
Nỳvlt, O., Rausand, M.: Dependencies in event trees analyzed by petri nets. Reliab. Eng. Syst. Saf. 104, 45–57 (2012)
Ortmeier, F., Reif, W., Schellhorn, G.: Deductive cause-consequence analysis (DCCA). IFAC Proc. Vol. 38(1), 62–67 (2005)
Papazoglou, I.A.: Functional block diagrams and automated construction of event trees. Reliab. Eng. Syst. Saf. 61(3), 185–214 (1998)
Papazoglou, I.A.: Mathematical foundations of event trees. Reliab. Eng. Syst. Saf. 61(3), 169–183 (1998)
Rasmussen, J.: Trends in human reliability analysis. Ergonomics 28(8), 1185–1195 (1985)
Reisig, W.: Petri Nets: An Introduction, vol. 4. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-69968-9
Ridley, L.M.: Dependency modelling using fault-tree and cause-consequence analysis. Ph.D. thesis, Loughborough University, UK (2000)
Staley, J., Sutcliffe, P.: Reliability block diagram analysis. Microelectron. Reliab. 13(1), 33–47 (1974)
Wall, I.: Probabilistic risk assessment in nuclear power plant regulation. Nucl. Eng. Des. 60(1), 11–24 (1980)
Xin, B., Wan, L., Yu, J., Dang, W.: Basic event probability determination and risk assessment based on cause-consequence analysis method. In: Journal of Physics: Conference Series, vol. 1549, p. 052094. IOP Publishing (2020)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Abdelghany, M., Rashid, A., Tahar, S. (2024). A Framework for Formal Probabilistic Risk Assessment Using HOL Theorem Proving. In: Kohlhase, A., Kovács, L. (eds) Intelligent Computer Mathematics. CICM 2024. Lecture Notes in Computer Science(), vol 14960. Springer, Cham. https://doi.org/10.1007/978-3-031-66997-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-031-66997-2_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-66996-5
Online ISBN: 978-3-031-66997-2
eBook Packages: Computer ScienceComputer Science (R0)