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.
[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].
[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.
[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]}
