Fault trees (FT) are among the most prominent formalisms for reliability analysis of technical systems. Dynamic FTs extend FTs with support for expressing dynamic dependencies among components. The standard analysis vehicle for DFTs is state-based, and treats the model as a CTMC, a continuous-time Markov chain. This is not always possible, as we will explain, since some DFTs allow multiple interpretations. This paper introduces a rigorous semantic interpretation of DFTs. The semantics is defined in such a way that the semantics of a composite DFT arises in a transparent manner from the semantics of its components. This not only eases the understanding of how the FT building blocks interact. It also is a key to alleviate the state explosion problem. By lifting a classical aggregation strategy to our setting, we can exploit the DFT structure to build the smallest possible Markov chain representation of the system. The semantics - as well as the aggregation and analysis engine is implemented in a tool, called CORAL. We show by a number of realistic and complex systems that this methodology achieves drastic reductions in the state space.
|Number of pages||16|
|Journal||IEEE transactions on dependable and secure computing|
|Publication status||Published - Jun 2010|
- formal models
- EC Grant Agreement nr.: FP7-ICT-2007-1
- EC Grant Agreement nr.: FP7/214755
- Fault Trees