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


Share/Save/Bookmark

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.

[img]
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:
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

 

Repository Staff Only: item control page

Metis ID: 241898