A Rigorous, Compositional, and Extensible Framework for Dynamic Fault Tree Analysis

被引:98
作者
Boudali, Hichem [1 ]
Crouzen, Pepijn [2 ]
Stoelinga, Marielle [3 ]
机构
[1] European Space Agcy, Estec, TEC QQD, NL-2200 AG Noordwijk, ZH, Netherlands
[2] Univ Saarland, Dept Comp Sci, Fac Comp Sci, Dependable Syst & Software Grp, D-66123 Saarbrucken, Germany
[3] Univ Twente, Dept Comp Sci, Formal Methods & Tools Grp, NL-7500 AE Enschede, Netherlands
关键词
Fault trees; reliability; compositionality; formal models; framework;
D O I
10.1109/TDSC.2009.45
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Fault trees (FTs) 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 continuous-time Markov chain (CTMC). 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 is also 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.
引用
收藏
页码:128 / 143
页数:16
相关论文
共 27 条
[1]  
[Anonymous], 1994, Introduction to the Numerical Solutions of Markov Chains
[2]  
*AS 2 EMB COMP SYS, 2009, AS5506 AS2 EMB COMP
[3]   Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes [J].
Baier, C ;
Hermanns, H ;
Katoen, JP ;
Haverkort, BR .
THEORETICAL COMPUTER SCIENCE, 2005, 345 (01) :2-26
[4]   Compositional Dependability Evaluation for STATEMATE [J].
Boede, Eckard ;
Herbstritt, Marc ;
Hermanns, Holger ;
Johr, Sven ;
Peikenkamp, Thomas ;
Pulungan, Reza ;
Rakow, Jan ;
Wimmer, Ralf ;
Becker, Bernd .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2009, 35 (02) :274-292
[5]   Architectural dependability evaluation with Arcade [J].
Boudali, H. ;
Crouzen, P. ;
Haverkort, B. R. ;
Kuntz, M. ;
Stoelinga, M. I. A. .
2008 IEEE INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS & NETWORKS WITH FTCS & DCC, 2008, :512-+
[6]  
BOUDALI H, 2007, P ARTIST WS TOOL PLA
[7]  
Boudali H, 2007, LECT NOTES COMPUT SC, V4762, P441
[8]   Dynamic fault tree analysis using Input/Output interactive Markov chains [J].
Boudali, Hichem ;
Crouzen, Pepijn ;
Stoelinga, Marieelle .
37TH ANNUAL IEEE/IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS, PROCEEDINGS, 2007, :708-+
[9]  
BOYD MA, 1991, THESIS DUKE U
[10]   The theory of interactive generalized semi-Markov processes [J].
Bravetti, M ;
Gorrieri, R .
THEORETICAL COMPUTER SCIENCE, 2002, 282 (01) :5-32