Dynamic fault trees (DFTs) are a versatile and common formalism to model and analyze the reliability of computer-based systems. This paper presents a formal semantics of DFTs in terms of input/output interactive Markov chains (I/O-IMCs), which extend continuous-time Markov chains with discrete input, output and internal actions. This semantics provides a rigorous basis for the analysis of DFTs. Our semantics is fully compositional, that is, the semantics of a DFT is expressed in terms of the semantics of its elements (i.e. basic events and gates). This enables an efficient analysis of DFTs through compositional aggregation, which helps to alleviate the state-space explosion problem by incrementally building the DFT state space. We have implemented our methodology by developing a tool, and showed, through four case studies, the feasibility of our approach and its effectiveness in reducing the state space to be analyzed. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Boudali, H., Crouzen, P., & Stoelinga, M. (2007). A compositional semantics for dynamic fault trees in terms of interactive Markov chains. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4762 LNCS, pp. 441–456). Springer Verlag. https://doi.org/10.1007/978-3-540-75596-8_31
Mendeley helps you to discover research relevant for your work.