Introduction to Specification and Verification
5
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.
Exam
15.12.2014
16.00
CK112
| Year | Semester | Date | Period | Language | In charge |
|---|---|---|---|---|---|
| 2014 | autumn | 27.10-10.12. | 2-2 | English | Timo Karvi |
Lectures
| 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
| Time | Room | Instructor | Date | Observe |
|---|---|---|---|---|
| Wed 12-14 | C222 | Timo Karvi | 03.11.2014—12.12.2014 |
General
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:
- Introduction
- Labelled transition systems
- Global state graph
- Principles in modelling
- Trace and bisimulation equivalences
- Basic Lotos
- Full Lotos
- Full Lotos examples
- 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.