Introduction to Specification and Verification

Hajautetut järjestelmät ja tietoliikenne
Syventävät opinnot
The course introduces some basic concepts and techniques in the verification of distributed systems: labelled transition graphs, global state graph, trace and bisimulation equivalences, basic Lotos and linear temporal logic. Moreover, the CADP spesification and verification software will be used in the exercises.


15.12.2014 16.00 CK112
Vuosi Lukukausi Päivämäärä Periodi Kieli Vastuuhenkilö
2014 syksy 27.10-10.12. 2-2 Englanti Timo Karvi


Aika Huone Luennoija Päivämäärä
Ma 12-14 C222 Timo Karvi 27.10.2014-10.12.2014
Ke 10-12 C222 Timo Karvi 27.10.2014-10.12.2014


Group: 1
Aika Huone Ohjaaja Päivämäärä Huomioitavaa
Ke 12-14 C222 Timo Karvi 03.11.2014—12.12.2014



This is a Master's programme -level course which is especially suitable for students in Distributed systems and data communication and Software systems sub-programmes, but also in Algorithms and machine learning sub-programme.


The course consists of the following topics:

  1. Introduction
  2. Labelled transition systems
  3. Global state graph
  4. Principles in modelling
  5. Trace and bisimulation equivalences
  6. Basic Lotos
  7. Full Lotos
  8. Full Lotos examples
  9. Linear  and branching time temporal logic


Kurssin suorittaminen

 Exercises are compulsory and produce extra points. It is necessary to solve 40% of the exercises and this produces one point. 80% produces 10 points. It has been planned that some of the exercises are returned to the assistant to be checked. If this practice is applied widely, then the amount of points the exercises produce will increase. The practice is decided in the first lecture, when it is clear how many students are taking part in the course.

There are two course exams and two separate exams. In the course exams, the maxmimum amount of points is 50 and to this the points got from the exercises are added. The second course exam (January-February) is at the same time a separate exam, where the exercise points are not counted (the best alternative is taken into account). The third exam is late in the spring and the last in summer. In these last two exams the exercise points are no more counted.

Kirjallisuus ja materiaali

The material consists of lecture notes and exercises.

Obs! Some chapters are missing in the Lecture Notes, but they are instead in the slides. See the exercise page.