The course spans the period E4A (Fall, see DTU’s academic calendar).
Lectures and tutorials take place in building 324, room H060 every Tuesday, from 13:00 to 17:00.
The
oral exam will be on December 12-14 (please double-check with DTU
examination page),
and possibly some day around if needed.
The basic idea behind model checking is that we have
a mathematical model of a system (software, hardware, biological, …) and
some property that we want to verify. The model is an abstract description of
what the system does (this could be manually or automatically derived from
either a specification or an actual system), and the property is a
description of what the system should do (possibly derived from some
requirements specification and expressed in specification languages called
temporal logics). A model checker is a software tool that will take any
model in a given formalism, and any property in a given logic, and will automatically
verify that property.
1.
Every time we connect to a
website, or use our mobile phone, or fly on an airplane, we are relying on
highly complex distributed or embedded systems. As many aspects of our lives
depend upon such systems, we need them to be reliable – both in the sense of doing
what we expect them to do, and being fast enough to meet our expectations.
Model checking allow us to answer these questions, and in doing so build more
robust and reliable
systems.
2. Model checking is used by key international IT companies (Intel, Microsoft, Amazon, etc.) to provide highly reliable systems and services. It is indeed a unique design, analysis and development skill that that internationally leading software and hardware companies need for engineering safe and secure systems systems and services.
3.
Model checking is a perfect complement to other
design, analysis and development techniques covered at courses offered at DTU
like program analysis and compiler
construction.
4. Model checking is not
limited to IT systems: it can be applied in many other domains like biology,
medicine, finance, and social sciences.
We look at different types of models and properties, and a supplementary third part presenting a wider view of the field but in less detail.
Discrete models and logics
We use discrete models when we are concerned with the possibility of something happening, as it lets us model all the possible eventualities without considering how likely each one is. This is typically used for systems that we have complete control over, and so we want to ensure that they are free of bugs. For example, is it possible for a mobile phone to crash? Or, is it possible for a word processor to suddenly stop responding?
We will introduce something called a Kripke structure as our modeling formalism. This is basically a finite state machine whose states are labelled, and whose transitions are non-deterministic (hence we take into account all possible eventualities). We will introduce Computation Tree Logic (CTL) as a way of specifying properties, and look at the CTL model checking algorithm, although our focus will be on practical applications of model checking. We will also think about what it means for two models to behave in an equivalent way, by learning about a concept called bisimulation. This is important for both comparing models and reducing the size of their state space (making it easier to verify them).
Stochastic models and logics in discrete time
Sometimes we don't have complete control of a system, because the environment it runs in is not predictable. When we buy a ticket online, there is a chance that the network could fail half way through the transaction – for example, a tree might fall down and break a cable. Since there is always the possibility of something going wrong, a more interesting question is to ask what the probability of something happening is.
We
will introduce a modelling formalism called a Discrete Time Markov Chain (DTMC).
This can be thought of as putting probabilities on the transitions of the
Kripke structures from Part I. We will review some basic probability theory,
and look at the behaviour of a DTMC as it evolves over time (transient
analysis), and after it has run for a long time (steady state analysis).
Building on this foundation, we will introduce a logic called Probabilistic
CTL (PCTL), and how to do model checking for it. This is an extension of
CTL in which we can ask questions like "can I be 99.99% certain that the
system won't crash before my ticket is booked?" We will extend the notion
of bisimulation from Part I to DTMCs, and briefly look at what happens when we
have both probabilistic and non-deterministic behaviour in a model.
Games
In
some systems we may have different sources of uncertainty that require a
specific treatment: as above some may be of a probabilistic nature due to the
use of randomized strategies or because we have an estimate of their
non-deterministic behavior, we could also have non-deterministic behaviours that are either due to non-controllable factors
(e.g. the system’s environment) or underspecified
parts of the system to be refined.
In this part of the course we will introduce Markov Decision Processes and Stochastic Games as models that allows us to consider all such aspects and we will see how logics and algorithms can be used to solve control and game problems.
Throughout this course, there will be a strong
emphasis on the practical application of model checking, and we will make use
of the PRISM model
checker. This provides a higher level modelling language that maps
onto all the mathematical formalisms we have seen so that we do not need to
work with them directly. The aim is to develop a firm understanding of the
theory of model checking, but also to gain practical experience. There will be
mandatory assignments, for which there will be a written report, and this will
be the basis of the oral exam.
· [BK08]
Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT
Press.
o You can purchase the book from the university book store.
o You can find the book
online in other shops.
o
Please find errata for the book here.
·
The PRISM and PRISM-GAMES model
checkers.
·
The Z3
solver.
·
02246 page on DTU Kursusbasen
·
02246 on DTU Learn (search for 02246)
· 02246 on Inside (search for 02246)