Introduction to Specification and Verification

581366
5
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.

Koe

16.12.2011 16.00 A111
Vuosi Lukukausi Päivämäärä Periodi Kieli Vastuuhenkilö
2011 syksy 01.11-08.12. 2-2 Englanti Timo Karvi

Luennot

Aika Huone Luennoija Päivämäärä
Ti 16-18 D122 Timo Karvi 01.11.2011-08.12.2011
To 16-18 D122 Timo Karvi 01.11.2011-08.12.2011

Harjoitusryhmät

Group: 1
Aika Huone Ohjaaja Päivämäärä Huomioitavaa
To 14-16 B222 Timo Karvi 31.10.2011—09.12.2011

Yleistä

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

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.

A short summary about the material you should know.

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

Kirjallisuus ja materiaali

The material consists of lecture notes and exercises.