A Framework for Formal Probabilistic Risk Assessment Using HOL Theorem Proving

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.