Formalization of RBD-based Cause Consequence Analysis in HOL

EasyChair Preprint 5720

Abstract

Cause consequence analysis is a safety assessment technique that is traditionally used to model the causes of subsystem failures in a critical system and their potential consequences using Fault Tree and Event Tree (ET) dependability modeling techniques, combined in a graphical Cause-Consequence Diagram (CCD). In this paper, we propose a novel idea of using Reliability Block Diagrams (RBD) for CCD analysis based on formal methods. Unlike Fault Trees, RBDs allow to model the success relationships of subsystem components to keep the entire subsystem reliable. To this end, we formalize in higher-order logic new mathematical formulations of CCD functions for the RBD modeling of generic n-subsystems using HOL4. This formalization enables universal n-level CCD analysis, based on RBDs and ETs, by determining the probabilities of multi-state safety classes, i.e., complete/partial failure and success, that can occur in the entire complex systems at the subsystem level.

Keyphrases: Cause-Consequence Analysis, Cause-Consequence Diagram, Event Tree, Reliability Block Diagram, complex system, critical system, dependability modeling technique, higher-order logic, theorem proving

@booklet{EasyChair:5720,
  author    = {Mohamed Abdelghany and Sofiene Tahar},
  title     = {Formalization of RBD-based Cause Consequence Analysis in HOL},
  howpublished = {EasyChair Preprint 5720},
  year      = {EasyChair, 2021}}