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
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.
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
Instructor:
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%).
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
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
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
Monday 27/04/2009
· 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,
Tuesday 28/04/2009
Wednesday 28/04/2009