The course spans the period E4A (Fall, see DTU’s academic calendar).
Lectures and tutorials take place in building 306, room H31 every Tuesday, from 13:00 to 17:00.
The oral exam will
be on December 15, and possibly some day around if needed (most
likely the December 16).
The basic idea
behind model checking is that we have a mathematical model of a software and/or
hardware system, 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 implementation), 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 computer 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.
The course is split into two main parts, in which we look at two different types of models and properties, and a supplementary third part presenting a wider view of the field but in less detail.
Part I: 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?
In this part of the course, 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 nondeterministic (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).
Part II: 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.
In this part of the course, 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 nondeterministic behaviour in a model.
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 – transition systems and DTMCs – 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 two mandatory assignments, for which there will be a
written report, and this will be the basis of the oral exam.
· [BK08]
Christel Baier and JoostPieter Katoen, Principles of Model Checking, MIT
Press.
o You can purchase the book here, from the university book store.
o Please find errata for the book here.
· Course
handouts will be distributed during the lectures; they may be used as a substitute
for [BK08] but we do recommend that you buy the book.
·
Example files for PRISM will
be made available on CampusNet under File sharing.
·
The PRISM model
checker.
Meeting 
Date 
Lecturer 
Topic 
Reading Material 
Supplementary Material (on Campus Net) 
01

1/9 
Alberto 
Introduction 
Slides Lecture 00 Mandatory
Assignment Part 0 Files FCFS.nm, FCFS.pctl, SRT.nm and SRT.pctl Slides Lecture 00 

02 
8/9 
Alberto 
Transition Systems 
Chapter 2 of [BK08] 
Mandatory Assignment Part 1 Slides Lecture 01 
03 
15/9 
Alberto 
Computation Tree Logic (CTL) 
Sections 6, 6.1, 6.2 of [BK08] and a bit of 6.8 of [BK08]. 
Slides Lecture 02 
04 
23/9 
Alberto 
CTL Model Checking 
Section 6.4 
Slides Lecture 03 
05 
29/9 
Alberto 
Bisimulation 
Sections 7, 7.1.1, 7.2 of [BK08]. 
Slides Lecture 04 
06 
6/10 
Alberto 
Work on Mandatory
Assignment 1 


19/10 

Hand in Mandatory
Assignment 1 


07 
20/10 
Alberto 
Discrete Time Markov Chains 
Sections 10, 10.1 of [BK08] 
Mandatory
Assignment Part 1 Slides Lecture 05 
08 
27/10 
Alberto 
Probabilistic CTL 
Sections 10.1.1, 10.2 of [BK08] 
Slides Lecture 06 
09 
3/11 
Alberto 
PCTL Model Checking 
Sections 10.1.1, Section 10.2.1, Section 10.2.2 of [BK08] 
Slides Lecture 07 
10 
10/11 
Alberto 
Probabilistic Bisimulation 
Section 10.4.2 of [BK08] 
Slides Lecture 08 
11 
17/11 
Alberto 
Work on Mandatory Assignment 2 

12 
24/11 
Alberto 
Beyond CTL and PCTL 

24/11 
Hand in Mandatory
Assignment 2 

13 
1/12 
Alberto 
Beyond CTL and PCTL 


17/12 
Alberto 
Oral exam 
· 02246 page on CampusNet (participants, materials, etc.)
· 02246 page on DTU Kursusbasen (general description)