OOTI Workshop on Model Checking and Static Analysis




About Model Checking and Static Analysis

Model checking is an approach to the verification of finite state programs. A program is unfolded into a transition system representing its state space, on which properties expressed in some form of temporal logic are then automatically checked to hold.

The paradigm enjoys an increasing acceptance by industry, as is underlined by the widespread use of model checking tools. One such tool is Spin, developed by Gerard Holzmann at Bell Labs in Murray Hill, NJ. Look here for more information on the tool.

This model checking part of the course is centered around the Spin tool. Several concepts and methods in the area of model checking are introduced and exemplified with the help of concrete examples.

Like model checking, static code analysis is an automated technique that is used to analyze programs without executing them. Unlike model checking, static analysis does not require a model and works directly on the source code. For the static analysis parts of the code we will use the tool UNO.



During the workshop you will need to work with Spin and UNO and therefore the first step is to install those tools on your machine or some other computer that you are going to use. Installation instructions can be found on the corresponding web pages of the tool. You can ask your colleagues Rene en Vinh for help.

Practical Information

Location: HG 6.05a 

Dates and times:
Tuesday  21/04/2009, 09.00-12.30
Wednesday 22/04/2009,13.30-17.30
Thursday 23/04/2009, 09.00-12.30 and 13.30-17.30
Friday 24/04/2009, 9.00-12.30 and 13.30-17.30
Monday 25/04/2009, 9.00-12.30 and 13.30-17.30

Tuesday 27/04/2009, 13.30-17.30
Wednesday 28/04/2009, 13.30-17.30 

Dragan Bosnacki
room: WH 3.101 and HG 5.71
email: dragan@win.tue.nl
phone: +31 40 247 5159


Your mark will be based on the first assignment (together 25%), and the second (final) assignment (75%).

Topics and Schedule

Some Acknowledgments and Literature: To a great extent this course has been given as developed and thought by Dennis Dams in 1997 and 1998, and earlier by Rob Gerth. The written materials that are on this page are mostly from the book Design and Validation of Computer Protocols by Gerard Holzmann, denoted in the sequel as [Hol91]. If you want to know more about model checking, there are nice books that can be found on the Spin web page.

Besides the lectures, number of exercises will be made in hands-on sessions. The (tentative) schedule is as follows. During the course, specific material will be made available in this section.

Tuesday 21/04/2009

  • About the course
  • Formal Methods, Model Checking, Spin  (reading: Intro summary)
  • A quick start with Spin: a Mutual Exclusion Protocol .
  • Study on-line documentation.
  • Slides, Day 1
  • reading: The whole Section 1, the introduction to Section 2 (up to subsection 2.1),  and optionally Section 4 (up to 4.2) from the paper:

The Spin Model Checker by Gerard Holzmann,
IEEE Trans. on Software Engineering,
Vol. 23, No. 5, May 1997, pp. 279-295.
(gzipped postscript)(PDF)


The paper also can be downloaded from Spin’s web page section titled Theoretical Background.


Wednesday 22/04/2009


Thursday 23/04/2009

·        Discussion of the exercise (Dijkstra-Dekker Mutual Exclusion Protocol)

·        LTL continued

·        Büchi automata

·        Translating LTL to Büchi automata

·        Verifying properties with LTL

·        Exercise: Leader Election Protocol (LEP), Introduction to Spin with LEP as an Example by Joost-Pieter Katoen

·        First Assignment

·        Slides, Day 3


Friday 24/04/2009

·        Discussion First Assignment

·        Weak Fairness (Example, Property), Strong Fairness (Example, Property1, Property2)

·        “Advanced” Promela

·        Reduction Techniques: Approximate Reduction (Bit-State Hashing, Hash Compatct), Minimized Automaton, Partial Order Reduction

·        Finding Cycles, Nested Depth-First Search

·        Second Assignment

·        Slides, Day 4

Monday 27/04/2009

·        Pathfinder

·        Static Code Analysis and Uno

·        Static Analysis via Model Checking, Basics

·        Property automata in Uno

·        Reading (see Uno’s web page, under Documentation) :

 Static source code checking for user-defined properties
G.J. Holzmann
Proc. IDPT 2002, Pasadena CA USA, June 2002.

·        Slides, Day 5

Tuesday 28/04/2009

Wednesday 28/04/2009


This is an adaptation of the page previously created by Dennis Dams, for the same OOTI SPIN workshop.
It has been maintained by Dragan Bosnacki.