Modelling, Specification, and Verification of Distributed Systems VT'07, 5p

19-20 april, 8-9 maj, och 29-30 maj, 2007.

Contents , Schedule , Examination , Course Material , Info on SPIN


Software systems are becoming an important part of the infrastructure of our society. Correctness and reliability have become issues of outmost importance. Testing and correction of software systems are irksome processes which typically consume half of the resources for system development. Thus, we need tools for analyzing software systems with the purpose of checking that they conform to their intended behavior, and for locating imperfections (``bugs'') that will cause run-time errors, security vulnerabilities, crashes, undelivered functionality, etc.

This course concentrates on techniques to verify and find bugs in concurrent and parallel software systems. Problems that arise from the parallel execution of several threads, processes, or components are particularly hard to find a diagnose. In particular, the course teaches model checking. Model checking techniques can automatically analyze a pseudo-code description of a communication protocol, a concurrent algorithm, etc. and find all potential errors. The course will also cover basics of structured testing for concurrent and parallel software, as well verification of software.

The material will be practically demonstrated with the tool SPIN. Spin supports a high level language to specify systems descriptions, called PROMELA (a PROcess MEta LAnguage). Spin has been used to trace logical design errors in distributed systems design, such as operating systems, data communications protocols, switching systems, concurrent algorithms, railway signaling protocols, etc. The tool checks the logical consistency of a specification. It reports on deadlocks, unspecified receptions, flags incompleteness, race conditions, and unwarranted assumptions about the relative speeds of processes. Spin can also be used to illustrate techniques in structured software testing, and has an extension to extract verification models from ANSI-C code.


The course is conducted in three two-day sessions. The topics covered at each session are:

First Session, April 19-20
The first session will cover modeling, specification, and verification, using the paradigm of linear-time temporal logic and the "automata-theoretic approach". It will also cover the SPIN tool and the Promela language, which are built on these concepts.

Second Session, May 8-9
The second session will cover algorithms that make the verification of correctness properties efficient. It will show how to optimize models to make them amenable to verification. Specific classes of protocols, distributed algorithms, etc. will be presented, modeled, and discussed from the point of view of verification. Third Session, May 29-30
The third session will briefly cover extensions of the verification techniques to cover test generation and verification of software (given in ANSI-C). For the verification of ANSI-C programs, there is an extension of SPIN, ModEx, which transforms C programs into Promela to allow formal verification. The course will use the
SPIN tool.

Preliminary Schedule


The following are part of examination

Homework Assignments

Course Material

Course material covering the different parts of the course:

SPIN: some information.

Reference Material

Following are papers and books that are relevant for the course.