Tutorial T7
QoS Modeling and Verification with UML Statecharts
Holger Hermanns
(Saarland Univ., Germany)
David N. Jansen
(Univ. of Twente, The Netherlands)
Joost-Pieter Katoen
(RWTH Aachen, Germany)
Duration: 180 minutes
The UML is an influential and widespread notation for high-level modelling of information processing system. UML statechart diagrams are a graphical language to describe system behaviour. They constitute one of the most intensively used formalisms comprised by the UML. However, statechart diagrams are lacking concepts for describing real-time, performance, dependability and QoS characteristics at a behavioural level.

In this tutorial, we present a QoS-oriented extension of UML statechart diagrams, called StoCharts. StoCharts enhance the basic statechart formalism with two distinguished features, both being simple and easy to understand, yet powerful enough to model a sufficiently rich class of stochastic decision processes. This is illustrated by a selection of case studies performed using StoCharts. We review the main ingredients of StoCharts and explain different approaches to evaluate QoS requirements satisfied by a collection of StoCharts. In particular we emphasize how a rigid formal semantics makes it possible to employ stochastic model checking to verify QoS requirements.

Web Maintenance Person.