12th Estonian Winter School in Computer Science (EWSCS)
XII Eesti Arvutiteaduse Talvekool
Palmse, Estonia, March 4-9, 2007
under the auspices of European Educational Forum
Anna Ingólfsdóttir
Dept. of Computer ScienceReykjavík University
Iceland
Reactive Systems: Modelling, Specification and Verification
Abstract
In this course we introduce three of the basic notions that we shall use to describe, specify and analyze reactive systems, namely
- Milner's Calculus of Communicating Systems (CCS, Milner 1989),
- the model of Labelled Transition Systems (LTSs, Keller 1976), and
- Hennessy-Milner Logic (HML, Hennessy and Milner 1985) and its extension with recursive definitions of formulae (Larsen1990).
We shall present a general theory of reactive systems and its applications. In particular, we intend to show how to describe actual systems using terms in our chosen models (that is, either as terms in the process description language CCS or as labelled transition systems), to offer specifications of the desired behaviour of systems either as terms of our models or as formulae in HML. We also show how to manipulate these descriptions, possibly (semi-)automatically, in order to analyze the behaviour of the model of the system under consideration.
Course materials
- L. Aceto, A. Ingólfsdóttir, K. G. Larsen, J. Srba. Draft of Part I: A classic theory of reactive systems of the book Reactive systems: modelling, specification and verification, to appear.
- A. Ingólfsdóttir. Reactive systems: modelling, specification and verification. Slides. Part 1 [pdf], part 2 [pdf], part 3 [pdf], part 4 [pdf], part 5 [pdf], part 6 [pdf], part 7 [pdf], part 8 [pdf], part 9 [pdf]