Extensions of statecharts with probability, time, and stochastic timing

Statecharts are a graphical language to describe the behaviour of a (computer) system. Statecharts are, among others, used as a part of the UML (Unified Modelling Language). This thesis describes three extensions related to statecharts. One of them is a real-time property language that fits well with statecharts. The two others extend the statechart language itself with probabilistic choice and stochastic timing. All languages have formal semantics that allow for automated analysis, for example model checking. The thesis shows how to apply these extensions with several examples: the real-time workflow of a travel office; a game taken from theoretical biology; whether a gambling machine satisfies the legal requirements; the efficiency of an automatic teller machine; and as the largest case study a part of a real-time network protocol where communication may fail with some probability. For all of these case studies, the system behaviour is described by one or several statecharts and analysesd using model checking or simulation.