Compositional Performability Evaluation for STATEMATE
Bernd Becker, Ralf Wimmer, Reza Pulungan, Thomas Peikenkamp, Sven Johr, Holger Hermanns, Marc Herbstritt, Eckard Böde, Bernd Becker, Ralf Wimmer, Reza Pulungan, Thomas Peikenkamp, Sven Johr, Holger Hermanns, Marc Herbstritt, Eckard Böde · 2006
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