Formal Probabilistic Risk Assessment using Theorem Proving
Mohamed Abdelghany and Sofiene Tahar
Contact: m_eldes@encs.concordia.ca
The central inquiry in many safety-critical systems is to assess the probability of all possible risk consequences that can occur in a system and its subsystems. The two main methods commonly used by planners/designers for evaluating the risk assessment probabilities are Event Tree Analysis (ETA) and Fault Tree Analysis (FTA). In this research, we use the higher-order logic theorem prover HOL4 to formalize Event Trees (ET), Functional Block Diagrams (FBD) and Cause Consequence Diagrams (CCD) based on Fault Trees (FT) as well as on Reliability Block Diagrams (RBD), as a novel approach. Moreover, we developed a Functional Block Diagrams and Event Trees Modeling and Analysis (FETMA) software tool in Python, which provides user-friendly features and graphical interfaces for industrial design engineers. We applied our methods and tools on several real-world case studies from the smart grid power systems sector, such as an IEEE 118-Bus Transmission Power Network, an Interconnected Micro-Grids System, a Nuclear Power Plant, etc.
Mohamed Wagdy Eldesouki Abdelghany, "Formal Probabilistic Risk Assessment using Theorem Proving with Applications in Power Systems", PhD Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, September 2021
[1] M. Abdelghany, W. Ahmad, and S. Tahar, "Event Tree Reliability Analysis of Safety Critical Systems using Theorem Proving," IEEE Systems Journal, Vol. 16, No. 2, June 2022, pp. 2899-2910.
[2] M. Abdelghany and S. Tahar, "Cause-Consequence Diagram Reliability Analysis using Formal Techniques with Application to Electrical Power Networks," IEEE Access, Vol. 9, January 2021, pp. 23929-23943.
[1] M. Abdelghani and S. Tahar: Formalization of RBD-based Cause Consequence Analysis in HOL; In: F. Kamareddine and C. Sacerdoti Coen (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 12833, Springer, 2021, pp. 47-64. [Proc. Conference on Intelligent Computer Mathematics (CICM'21), Timisoara, Romania, July 2021].
[2] M. Abdelghany, W. Ahmad, and S. Tahar, "Event Tree Reliability Analysis of Electrical Power Generation Network using Formal Techniques," in Electric Power and Energy Conference. IEEE, November 2020, pp. 1-7.
[3] M. Abdelghany, W. Ahmed and S. Tahar: ETMA: An Efficient Tool for Event Trees Modeling and Analysis; Proc. IEEE International Systems Conference (SysCon'20), Montreal, Quebec, Canada, August 2020, pp. 1-8.
[4] M. Abdelghany and S. Tahar: Formalization of Functional Block Diagrams using HOL Theorem Proving; In L. Lima and V. Molnár (Eds.), Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 13768, Springer Verlag, 2022, pp. 22-35. [Proc. Brazilian Symposium on Formal Methods (SBMF'22), Brazil, December, 2022]
[5] M. Abdelghany and S. Tahar. Tahar: Formal Probabilistic Risk Assessment of a Nuclear Power Plant; Proc. ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'22), Auckland, New Zealand, December 2022, pp. 80-87.
[1] M. Abdelghany, and S. Tahar: Formal FT-based Cause-Consequence Reliability Analysis using Theorem Proving; Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2021. [41 Pages]. {Formal Languages and Automata Theory, arXiv.2101.07174 [arxiv]}
[2] M. Abdelghany, W. Ahmad, and S. Tahar: ETMA: A New Software for Event Tree Analysis with Application to Power Protection; Technical Report, Department of Electrical and Computer Engineering, Concordia University, June 2020. [21 Pages]. {Computing Research Repository (CoRR), Electrical Engineering and Systems Science, Signal Processing, arXiv:2006.12383} [arxiv]}
[3] M. Abdelghany, W. Ahmad, and S. Tahar: A Formally Verified HOL4 Algebra for Event Trees; Technical Report, Department of Electrical and Computer Engineering, Concordia University, April 2020. [17 Pages]. {Computing Research Repository (CoRR), Electrical Engineering and Systems Science, Systems and Control, arXiv.2004.14384} [arxiv]}
[1] M. Abdelghany and S. Tahar: Reliability Analysis of Smart Grids Using Formal Methods; In: M. Fathi et al. (Eds.), Handbook of Smart Energy Systems, pp. 1-15, Springer, 2022. (ISBN: 978-3-030-72322-4)
Publications
[1] M. Abdelghany, W. Ahmad, and S. Tahar, "Event Tree Reliability Analysis of Safety Critical Systems using Theorem Proving," IEEE Systems Journal, Vol. 16, No. 2, June 2022, pp. 2899-2910.
[2] M. Abdelghany and S. Tahar, "Cause-Consequence Diagram Reliability Analysis using Formal Techniques with Application to Electrical Power Networks," IEEE Access, Vol. 9, January 2021, pp. 23929-23943.
[1] M. Abdelghani and S. Tahar: Formalization of RBD-based Cause Consequence Analysis in HOL; In: F. Kamareddine and C. Sacerdoti Coen (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 12833, Springer, 2021, pp. 47-64. [Proc. Conference on Intelligent Computer Mathematics (CICM'21), Timisoara, Romania, July 2021].
[2] M. Abdelghany, W. Ahmad, and S. Tahar, "Event Tree Reliability Analysis of Electrical Power Generation Network using Formal Techniques," in Electric Power and Energy Conference. IEEE, November 2020, pp. 1-7.
[3] M. Abdelghany, W. Ahmed and S. Tahar: ETMA: An Efficient Tool for Event Trees Modeling and Analysis; Proc. IEEE International Systems Conference (SysCon'20), Montreal, Quebec, Canada, August 2020, pp. 1-8.
[4] M. Abdelghany and S. Tahar: Formalization of Functional Block Diagrams using HOL Theorem Proving; In L. Lima and V. Molnár (Eds.), Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 13768, Springer Verlag, 2022, pp. 22-35. [Proc. Brazilian Symposium on Formal Methods (SBMF'22), Brazil, December, 2022]
[5] M. Abdelghany and S. Tahar. Tahar: Formal Probabilistic Risk Assessment of a Nuclear Power Plant; Proc. ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'22), Auckland, New Zealand, December 2022, pp. 80-87.
[1] M. Abdelghany, and S. Tahar: Formal FT-based Cause-Consequence Reliability Analysis using Theorem Proving; Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2021. [41 Pages]. {Formal Languages and Automata Theory, arXiv.2101.07174 [arxiv]}
[2] M. Abdelghany, W. Ahmad, and S. Tahar: ETMA: A New Software for Event Tree Analysis with Application to Power Protection; Technical Report, Department of Electrical and Computer Engineering, Concordia University, June 2020. [21 Pages]. {Computing Research Repository (CoRR), Electrical Engineering and Systems Science, Signal Processing, arXiv:2006.12383} [arxiv]}
[3] M. Abdelghany, W. Ahmad, and S. Tahar: A Formally Verified HOL4 Algebra for Event Trees; Technical Report, Department of Electrical and Computer Engineering, Concordia University, April 2020. [17 Pages]. {Computing Research Repository (CoRR), Electrical Engineering and Systems Science, Systems and Control, arXiv.2004.14384} [arxiv]}
[1] M. Abdelghany and S. Tahar: Reliability Analysis of Smart Grids Using Formal Methods; In: M. Fathi et al. (Eds.), Handbook of Smart Energy Systems, pp. 1-15, Springer, 2022. (ISBN: 978-3-030-72322-4)
