  Cause-consequence Diagram (CCD) is widely used as a deductive safety analysis
technique for decision-making at the critical-system design stage. This
approach models the causes of subsystem failures in a highly-critical system
and their potential consequences using Fault Tree (FT) and Event Tree (ET)
methods, which are well-known dependability modeling techniques.
Paper-and-pencil-based approaches and simulation tools, such as the Monte-Carlo
approach, are commonly used to carry out CCD analysis, but lack the ability to
rigorously verify essential system reliability properties. In this work, we
propose to use formal techniques based on theorem proving for the formal
modeling and step-analysis of CCDs to overcome the inaccuracies of the
simulation-based analysis and the error-proneness of informal reasoning by
mathematical proofs. In particular, we use the HOL4 theorem prover, which is a
computer-based mathematical reasoning tool. To this end, we developed a
formalization of CCDs in Higher-Order Logic (HOL), based on the algebraic
approach, using HOL4. We demonstrate the practical effectiveness of the
proposed CCD formalization by performing the formal reliability analysis of the
IEEE 39-bus electrical power network. Also, we formally determine the Forced
Outage Rate (FOR) of the power generation units and the network reliability
index, i.e., System Average Interruption Duration Index (SAIDI). To assess the
accuracy of our proposed approach, we compare our results with those obtained
with MATLAB Monte-Carlo Simulation (MCS) as well as other state-of-the-art
approaches for subsystem-level reliability analysis.
