  Dynamic fault trees (DFTs) have emerged as an important tool for capturing
the dynamic behavior of system failure. These DFTs are then analyzed
qualitatively and quantitatively using stochastic or algebraic methods to judge
the failure characteristics of the given system in terms of the failures of its
sub-components. Model checking has been recently proposed to conduct the
failure analysis of systems using DFTs with the motivation to provide a
rigorous failure analysis of safety-critical systems. However, model checking
has not been used for the DFT qualitative analysis and the reduction algorithms
used in model checking are usually not formally verified. Moreover, the
analysis time grows exponentially with the increase of the number of states.
These issues limit the usefulness of model checking for analyzing complex
systems used in safety-critical domains, where the accuracy and completeness of
analysis matters the most. To overcome these limitations, we propose a
comprehensive methodology to perform the qualitative and quantitative analysis
of DFTs using an integration of theorem proving and model checking based
approaches. For this purpose, we formalized all the basic dynamic fault tree
gates using higher-order logic based on the algebraic approach and formally
verified some of the simplification properties. This formalization allows us to
formally verify the equivalence between the original and reduced DFTs using a
theorem prover, and conduct the qualitative analysis. We then use model
checking to perform the quantitative analysis of the formally verified reduced
DFT. We applied our methodology to five benchmarks and the results show that
the formally verified reduced DFT was analyzed using model checking with up to
six times less states and up to 133000 times faster.
