Compositional Dependability Evaluation for STATEMATE

被引:26
作者
Boede, Eckard [1 ]
Herbstritt, Marc [2 ]
Hermanns, Holger [3 ]
Johr, Sven [3 ]
Peikenkamp, Thomas [1 ]
Pulungan, Reza [3 ]
Rakow, Jan [4 ]
Wimmer, Ralf [2 ]
Becker, Bernd
机构
[1] Inst Informat Technol, OFFIS, D-26121 Oldenburg, Germany
[2] Univ Freiburg, Fac Engn, D-79110 Freiburg, Germany
[3] Univ Saarland, Dept Comp Sci, D-66123 Saarbrucken, Germany
[4] Carl von Ossietzky Univ Oldenburg, Dept Comp Sci, D-26121 Oldenburg, Germany
关键词
Real-time and embedded systems; fault tolerance; modeling techniques; reliability; availability; serviceability; model checking; design notations and documentation; state diagrams; TIME;
D O I
10.1109/TSE.2008.102
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modeling tools like STATEMATE support safety and failure-effect analysis at design time, but restricted to qualitative properties. This paper reports on a (plug-in) extension of STATEMATE enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a highspeed train signaling system where the tool has been applied successfully.
引用
收藏
页码:274 / 292
页数:19
相关论文
共 43 条
[1]  
ABATE J, 1993, AEU-ARCH ELEKTRON UB, V47, P311
[2]  
[Anonymous], 1998, BINARY DECISION DIAG, DOI DOI 10.1007/978-1-4757-2892-7
[3]  
Asmussen S, 1996, SCAND J STAT, V23, P419
[4]   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
[5]   Model-checking algorithms for continuous-time Markov chains [J].
Baier, C ;
Haverkort, B ;
Hermanns, H ;
Katoen, JP .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) :524-541
[6]  
*BCG MIN, 2008, PROJ WEBS
[7]  
BLOM S, 2003, ENTCS, V89, P99
[8]  
Böde E, 2006, INT CONF QUANT EVAL, P167
[9]  
BOUALI A, 1992, P 4 INT WORK COMP AI, P96
[10]  
BRAYTON RK, 1996, P 8 INT C COMP AID V