A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains

Boudali, H. and Crouzen, P. and Stoelinga, M.I.A. (2007) A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains. In: 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), October 22-25, 2007, Tokyo, Japan.

Preview

PDF
322Kb

Abstract:	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.
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/64340
Official URL:	http://dx.doi.org/10.1007/978-3-540-75596-8_31
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 241898