Model Checking

• explain the characteristic features of a given system;
• explain the basic concepts of the process oriented approach to modelling, specification and validation/verification of systems;
• explain the covered modelling formalisms and use them to model systems;
• explain the covered logical specification formalisms and use them to specify properties related, e.g., to safety, security and performance;
• operate state-of-the-art verification tools and explain the overall workings of such tools;
• identify situations where the covered techniques apply;
• motivate and design a series of experiments using verification tools and interpret the results obtained;
• achieve the above goals in a group effort while at the same time maintaining individual accountability; and
• communicate his/her results in a clear and precise manner using a standard form for technical reports.

The course covers three main topics:
(1) Methods for modeling systems with features such as non-determinism, probabilistic/stochastic aspects, and multiple agents/objectives: transition systems, Markov models, and games.
(2) Logical formalisms for expressing properties related to the safety, security, and performance of systems.
(3) Validation and verification tools that determine the relationship between models and properties in order to establish strong guarantees related to safety, security, and performance.

02141, The students are expected to be familiar with finite automata and/or transition systems; this background can be obtained in the course 02141. The students are expected to have a basic knowledge about probability theory. The students must be able to write programs in a programming language.

Lectures, theoretical exercises, and practical exercises.