Compositional Dependability Evaluation for STATEMATE

Eckard Böde

doi:10.1109/TSE.2008.102

Compositional Dependability Evaluation for STATEMATE

2009-03-01

27

PRE

AI

DOI：10.1109/TSE.2008.102

Original

Original request for help

Save

Abstract

En 中文

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.

Keywords:

Real-time and embedded systems

fault tolerance

modeling techniques

reliability

availability

serviceability

model checking

design notations and documentation

state diagrams

Compositional Dependability Evaluation for STATEMATE

Abstract

Journal

Organization