The
course spans the period 30 August 2016 – 29 November 2016.
Lectures
and tutorials take place in building 303A, room 044 every Tuesday,
from 13:00 to 17:00.
The oral exam will be on December 15 and 16 in B324/R161.
Flemming Nielson, Alberto Lluch Lafuente.
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 much less detail.
Part I:
Discrete models and logics (56 blocks).
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). Finally we will take a brief
look at more expressive logics than CTL – in particular, a logic called CTL*.
Part II:
Stochastic models and logics in discrete time (56 blocks).
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.
o You can purchase the book here,
from the university book store.
o Please
find errata for the book here.
· The PRISM
model checker.
Meeting 
Date 
Lecturer 
Topic 
Reading
Material 
Supplementary
Material (on Campus Net) 
01 
30/8 
Flemming 
Introduction to the course. Overview of model checking and
software validation. Installing and using PRISM. 
Mandatory Assignment Part 0:
Background and Getting Started. Files FCFS.nm,
FCFS.pctl, SRT.nm and SRT.pctl. Slides Lect1 and Exe1. 

02 
6/9 
Flemming 
Transition Systems. 
Sections 2, 2.1, 2.2.1 and 2.2.6 of
[BK08]. 
Mandatory Assignment Part 1: Discrete
Modelling and Verification. Slides Lect2 and Exe2. 
03 
13/9 
Flemming 
Computation Tree Logic (CTL). 
Sections 6, 6.1, 6.2 of [BK08]. 
Slides Lect3 and Exe3. 
04 
20/9 
Flemming 
CTL Model Checking. 
Sections 6.4, a bit of 6.8 of [BK08]. 
Slides Lect4 and Exe4. 
05 
27/9 
Flemming 
CTL Model Checking. 
Sections 6.4, a bit of 6.8 of [BK08]. 
Slides Lect5 and Exe5. 
06 
4/10 
Flemming 
Bisimulation. 
Sections 7, 7.1.1, 7.2 of [BK08]. 
Slides Lect6 and Exe6. 

10/10 

Hand
in First Mandatory Assignment. 


07 
11/10 
Alberto 
Introduction to Markov chains. 
Sections 10, 10.1 of [BK08] 
Slides Lect7 and Exe 7. 
08 
25/10 
Alberto 
Probabilistic CTL, transient and
steady state distributions. Feedback session (mandatory assignment 1) 
Sections 10.1.1, 10.2 of [BK08] 
Slides Lect8 and Exe8 
09 
1//11 
Alberto 
The Qualitative Fragment of PCTL. 

Slides Lect9 and Exe9 
10 
8/11 
Alberto 
PCTL Model Checking. 
Sections 10.1.1, 10.2.1 of [BK08] 
Slides Lect10 and Exe10 
11 
15/11 
Alberto 
Probabilistic Bisimulation. 
Section 10.4.2 of [BK08] 
Slides Lect11 and Exe11 
12 
22/11 
Alberto 
Beyond CTL and PCTL. Work on the second mandatory
assignment. 


28/11 
Hand
in Second Mandatory Assignment. 

13 
29/11 
Flemming &
Alberto 
Beyond CTL and PCTL. 


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