Titel: Extensions of statecharts with probability, time, and stochastic timing

Auteur: David Nicolaas Jansen

Verdediging gepland op: 29 oktober 2003 15.00 uur

(met inleiding om 14.45 uur)

Faculteit: EWI

Afdeling: Informatica

Promotor: prof.dr. Roel Wieringa (leerstoel Informatiesystemen)

Assistent-promotor: dr. Joost-Pieter Katoen (leerstoel Formele Methoden en


Uitgever van het proefschrift: Inmarks AG, Bern, Zwitserland

Op de volgende tekst zal het praatje gebaseerd zijn:

How can an insurance company set quality standards? As there are always

difficult cases, it is unrealistic to require that all cases are handled

within some specific time. But at least, it may handle most cases within a

week. And, for VIP clients, within two days---if there are only a few VIP


Statecharts are a graphical language to describe the behaviour of a

(computer) system, for example the computer system of the insurance company.

With the extensions described in this book, the insurance company can

describe how much is ``most cases'' and how many are ``only a few VIP

clients''. It then can find a realistic quality standard by formal analysis

of the statecharts.

Tekst op de achterkant van het proefschrift:

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 Modeling 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 analysed using model checking or