Integrating DFT and DRBD Formalizations in HOL4

TL;DR

This paper integrates two formal modeling approaches, DFT and DRBD, within the HOL4 theorem prover to enable efficient and sound reliability analysis of complex engineering systems.

Contribution

It introduces a formal integration of DFT and DRBD in HOL4, with a proof of their algebraic equivalence, enhancing reliability analysis capabilities.

Findings

Formal proof of equivalence between DFT and DRBD algebras

Successful case study on a drive-by-wire system

Enhanced efficiency in formal reliability analysis

Abstract

Dynamic Fault Trees (DFT) and Dynamic Reliability Block Diagrams (DRBD) are two modeling approaches that capture the dynamic failure behavior of engineering systems for their reliability analysis. Recently, two independent higher-order logic (HOL) formalizations of DFT and DRBD algebras have been developed in the HOL4 theorem prover. In this work, we propose to integrate these two modeling approaches for the efficient formal reliability analysis of complex systems by leveraging upon the advantages of each method. The soundness of this integration is provided through a formal proof of equivalence between the DFT and DRBD algebras. We show the efficiency of the proposed integrated formal reliability analysis on a drive-by-wire system as a case study.