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.
Publications
Thesis
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
Journal Papers
[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.
Conference Papers
[1] M. Abdelghany, A. Rashid and S. Tahar: A Framework for Formal Probabilistic Risk Assessment using HOL Theorem Proving; In: A. Kohlhase and L. Kovács (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 14960, Springer Verlag, 2024, pp. 298–314. [Proc. Conference on Intelligent Computer Mathematics (CICM'24), Montreal, Canada, August 2024].
[2] 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]
[3] 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.
[4] 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].
[5] 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.
[6] 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.
Technical Reports
[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]}
Book Chapters
[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)
Applications
A - System-Level ET Reliability Analysis:
1) IEEE 3-Bus Composite Bulk Power System
The standard IEEE 3-bus of generation and transmission bulk power network is consisting of three main transmission lines (M), two lateral transmission lines (L), two generators (G), three (two step-up and one step-down) substations, and three different industrial, commercial and residential loads A, B and C. We conducted the formal system-level ET reliability analysis of the bulk power system.
2) Quebec-New England HVDC coupling system between Canada and US
We conducted the formal system-level probabilistic risk assessment of the Quebec-New England HVDC Transmission system operated by Hydro-Quebec power utility in Canada. The location of the Quebec-New England Phase II HVDC project (2,690 MW) has five terminals in order from North to South: Radisson, Nicolet, Des Cantons, Comerford, and Sandy Pond.
3) IEEE 118-Bus Transmission Power Network
Consider the standard IEEE 118-bus of a complex transmission power network representing a portion of the American electric power system (in the Midwestern US) consisting of 19 Generators (G), 186 Transmission Lines (TL), and 91 loads. We conducted the formal system-level probabilistic risk assessment of multiple ET load models simultaneously and verify some significant reliability and energy indices for the power network.
B - Subsystem-Level CCD Reliability Analysis:
1) 1- IEEE 39-Bus Distributed Generation Network
The standard IEEE 39-bus electrical power network is consisting of 10 generators (G), 12 substations (S/S), 39 Buses (Bus), and 34 transmission lines (TL). We used our CCD formalization in HOL4 to analyze all possible safety classes of reliability and failure consequence events that can occur in the electrical power network at the distributed generation subsystem level.
2) Interconnected Microgrid Renewable and Clean Power Grids
A smart power grid consists of four Interconnected Microgrid Renewable and Green (MRG) power grids incorporating 100% carbon-neutral green power plants, such as Wind Turbine (WT) and solar photo-voltaic (PV). We used our CCD formalization in HOL4 to analyze all possible safety classes of reliability and failure consequence events that can occur in the whole smart grid at each MRG subsystem level.
C - Subsystem-Level CCD Reliability Analysis:
1) Nuclear Power Plant:
In this application, we used our FBD formalization in the HOL4 to analyze the probabilities of all possible safety classes of accident events that can occur in the nuclear reactor at the subsystem level.
D - FETMA Software System/Subsystem-Level Reliability Analysi:
1) Transmission Line Protection Circuit Scheme
Consider a transmission line consists of 1 Distance Relay (R) and 1 Current Transformer (CT), 1 Potential Transformer (PT), 2 Trip Circuits (TC), and 2 Circuit Breakers (CB). Protective distance relays keep the utility grids and the equipment safe from faults and system unbalances by dividing the grid into zones. We used our proposed FETMA software to perform system-level ET reliability analysis of the transmission line protection scheme.
2) Smart Grid Automated Substation
Smart Automated Substations (SAS) of a smart power grid are constructed based on advanced monitoring infrastructure, control and protection devices, to operate as joint and multitask networks. We used our proposed FETMA software to analyze the probabilities of all possible classes of accident events that can occur in the SAS at each subsystem level (Process Level, Bay Level and Station Level).
