A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving.

Dependability analysis is an essential step in the design process of safety-critical systems, where the causes of failure and some other metrics, such as reliability, should be identified at an early design stage. The dynamic failure characteristics of real-world systems are usually captured by various dynamic dependability models, such as continuous time Markov chains (CTMCs), dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs). In order to conduct the formal dependability analysis of systems that exhibit dynamic failure behaviors, these models need to be captured formally. In this paper, we describe recent developments towards this direction along with a roadmap on how to be able to develop a framework for formal reasoning support for DFTs, DRBDs and CTMCs in a higher-order-logic theorem prover.