Download PDFOpen PDF in browser

Formalization of RBD-based Cause Consequence Analysis in HOL

EasyChair Preprint no. 5720

17 pagesDate: June 4, 2021


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, complex system, critical system, dependability modeling technique, Event Tree, higher-order logic, Reliability Block Diagram, theorem proving

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Mohamed Abdelghany and Sofiene Tahar},
  title = {Formalization of RBD-based Cause Consequence Analysis in HOL},
  howpublished = {EasyChair Preprint no. 5720},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser