Abstract

Dynamic fault trees (DFT) are widely used to analyze the fault-tolerance of computer systems. The syntax and semantics of DFT, however, lack formal definitions which has lead to vagueness in the interpretation of DFT. Existing analysis techniques also suffer from the state-space explosion problem.

This thesis describes a compositional approach to formalizing the DFT syntax and semantics. The DFT semantics are formalized by separating a DFT into its elements and formalizing the behavior of each element using an input/output interactive Markov chain (IOIMC). IOIMC are a combination of continuous-time Markov chains (CTMC) and input/output automata and IOIMC models can be combined using parallel composition. The semantics of a DFT are now defined as the composition of the semantics of its elements.

This compositional approach to formalizing DFT semantics also leads to the compositional analysis of DFT using compositional aggregation. Compositional aggregation is a well known technique which combines composition and aggregation to combat the state-space explosion problem.

In this thesis we give new formal definitions for the syntax and semantics of the DFT formalism. The IOIMC formalism is also introduced. Compositional analysis for DFT is then described which is accomplished using a translation tool (used to find IOIMC representations of DFT elements) and the Tipp tool. Two case studies are given that show the applicability of the new compositional analysis.

Additional Resources

1. The paper