Compositional Performability Evaluation for STATEMATE

Abstract— This paper reports on our efforts to link an industrial state-of-the-art modelling tool to academic state-of-the-art analysis algorithms. In a nutshell, we enable timed reachability analysis of uniform continuous-time Markov decision processes, which are generated from STATEMATE models. We give a detailed explanation of several construction, transformation, reduction, and analysis steps required to make this possible. The entire tool flow has been implemented, and it is applied to a nontrivial example. I. MOTIVATION This paper reports a success story. It is the story of how we managed to integrate very recent advances in stochastic model checking into a modelling environment with a stable industrial user group. The modelling environment is STATEMATE, a Statechart-based toolset used in several avionic and automotive companies like AIRBUS or BMW. The model checking is based on computing time bounded reachability probabilities, and allows us to verify properties like: “The ...

• Type: Conference
• Year: 2006
• Where: QEST
• Authors: Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd Becker
• Keywords: Enable Timed Reachability, Modelling Environment, QEST 2006, Quantitative Evaluation Of Systems, State-of-the-art Modelling Tool