Formal Dependability Analysis

Waqar Ahmed and Osman Hasan


Reliability Block Diagrams (RBDs) allow us to model the failure relationships of complex systems and their sub-components and are extensively used for system reliability, availability, dependability and maintainability analyses. Traditionally, these RBD-based analyses are done using paper-and-pencil proofs or computer simulations, which cannot ascertain absolute correctness due to their inherent limitations. As a complementary approach, we propose to use the higher-order-logic theorem prover HOL to conduct RBD-based analysis. For this purpose, we present a higher-order-logic formalization of commonly used RBD configurations, i.e., series, parallel, parallel-series and series-parallel, and the formal verification of their equivalent mathematical expressions. A distinguishing feature of the proposed RBD formalization, is the ability to model nested RBD structures, i.e., a RBD block could itself be a RBD. This generality allows us to formally analyze the reliability of many real-world systems. For illustration purposes, we have formally analyzed the reliabilities of a oil/gas pipeline, exhibiting the series RBD, and a generic Virtual Data Center (VDC) in a cloud computing infrastructure exhibiting the nested series-parallel RBD.


RBDs (a) Series (b) Parallel (c) Parallel-Series (d) Series-Parallel


  1. O. Hasan, W. Ahmed, S. Tahar and M. S. Hamdi, “Reliability Block Diagrams based Analysis: A Survey”, International Conference of Numerical Analysis and Applied Maths (ICNAAM-14), American Institute of Physics, Rhodes, Greece, 2014. To Appear.

  2. W. Ahmed, O. Hasan, S. Tahar and M. S. Hamdi, “Towards the Formal Reliability Analysis of Oil and Gas Pipelines”, Conferences on Intelligent Computer Mathematics (CICM-2014), Springer, LNAI 8543, Coimbra, Portugal, 2014, pp. 30–44.