Extensions of Statecharts with probability, time, and stochastic timing

D.N. Jansen

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    350 Downloads (Pure)


    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.
    Original languageUndefined
    Awarding Institution
    • University of Twente
    • Katoen, Joost P., Advisor
    • Wieringa, Roelf Johannes, Supervisor
    Thesis sponsors
    Award date29 Oct 2003
    Place of PublicationBern
    Print ISBNs3-9522850-0-5
    Publication statusPublished - 29 Oct 2003


    • EWI-1292
    • IR-58230

    Cite this