Introduction to Specification and Verification

Networking and Services
Advanced studies
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.


16.12.2011 16.00 A111
Year Semester Date Period Language In charge
2011 autumn 01.11-08.12. 2-2 English Timo Karvi


Time Room Lecturer Date
Tue 16-18 D122 Timo Karvi 01.11.2011-08.12.2011
Thu 16-18 D122 Timo Karvi 01.11.2011-08.12.2011

Exercise groups

Group: 1
Time Room Instructor Date Observe
Thu 14-16 B222 Timo Karvi 31.10.2011—09.12.2011


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. Linear time temporal logic

Completing the course

 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.

A short summary about the material you should know.

 Example exam 1. Example exam 2 (in Finnish). 

Literature and material

The material consists of lecture notes and exercises.