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.


15.12.2014 16.00 CK112
Year Semester Date Period Language In charge
2014 autumn 27.10-10.12. 2-2 English Timo Karvi


Time Room Lecturer Date
Mon 12-14 C222 Timo Karvi 27.10.2014-10.12.2014
Wed 10-12 C222 Timo Karvi 27.10.2014-10.12.2014

Exercise groups

Group: 1
Time Room Instructor Date Observe
Wed 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


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.

Literature and material

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.