Formalization of Reliability Block Diagrams in Higher-order Logic

Abstract: 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 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, such as 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 configurations, which are RBDs having blocks that also represent RBD configurations. This generality allows us to formally analyze the reliability of many real-world systems.

Technical Report: Waqar Ahmed, Osman Hasan and Sofiene Tahar. Formalization of RBD in HOL. NUST, Islamabad, Pakistan, 2016.
Proof Script: RBDScript

Waqar Ahmad is a PhD student at the School of Electrical Engineering and Computer Science of National University of Sciences and Technology. He is working on his PhD thesis in the System Analysis & Verification (SAVE) Lab of NUST-SEECS, under the supervision of Dr. Osman Hasan.