Model Checking, Summer semester 2009/2010
Lecturer: Dr. A. Sokolova, ana.sokolova"at"cs.uni-salzburg.at, office 2.17
Schedule: Tuesdays 10am-12am and 4pm-5pm in T06
First meeting: Tuesday, March 2 at 4pm in T06
Language: English
The course may also be taken by PhD students
Course description: Model checking is a technique for automatic
verification of finite state concurrent systems such as sequential circuit
designs and communication protocols. This method has advanced verification
from a purely theoretical to an also practically applicable discipline. Its inventors Edmund M. Clarke,
E. Allen Emerson, and
Joseph Sifakis have
been awarded the significant Turing award in 2007.
In this course we will learn the principles of model checking, namely
modeling with transition systems, the temporal logics LTL and CTL, their comparison,
as well as algorithms for verifying these logics. In addition, on
the practical side, we will get acquainted with the basics of the SPIN model checker,
one of the most commonly used model checking tools for automatic verification.
Literature:
The books can be ordered via Amazon.de . Some copies are available at
the department library.
Prerequisites: None, the course material is self-contained, as is the textbook.
Knowledge of basics of theoretical computer science like logic for computer science or automata theory is an asset.
Exam: This is a VP course. There will be three exam possibilities in June/July.
The exam is written consisting of several excersises from the material covered during the course. Additionally,
the homeworks and the
mini project will also contribute to the final grade.
Exam dates: First possibility: Tuesday 6.7.2010, 10am, T06. Second possibility: Thursday 22.7.2010, 10am, T06.
Third possibility: Tuesday 10.8.2010, 10am, T06.
Mini projects have been assigned, deadline for submitting a mini project is 1.8.2010
Useful links for the mini projects:
Schedule:
- Week 1, Tuesday 2.3.10: Introduction to Model Checking (Chapter 1 of
all books), first meeting.
- Week 2, Tuesday 9.3.10: Modelling (MC book p.13-25, PMC book p.26-88),
- Week 3, Tuesday 16.3.10: CTL* and LTL, syntax, semantics, examples
(MC book p.27-32, PMC book browse through Chapter 5).
- Week 4, Tuesday 23.4.10: Buechi Automata (properties), Model-based LTL model checking (MC book p.121-128).
- Week 5, Tuesday 13.4.10: LTL to GNBA translation algorithm (MC book p.132-138).
- Week 6, Tuesday 20.4.10: Emptiness check, strongly connected components--Tarjan's algorithm (MC book p.129-132, SIAM Journal of Computing 1(2) 1972 for Tarjan's algorithm)
- Week 7, Tuesday 27.4.10: Model checking CTL, labelling algorithm (MC book p. 35-40, 32-33)
- Week 8, Tuesday 4.5.10: Fairness, checking CTL with fairness, fixed points (MC book p. 40-41, 60-64)
- Week 9, Tuesday 11.5.10: Checking CTL via fixed points, BDDs (MC book p. 65-68, 51-53)
- Week 10, Tuesday 18.5.10: OBDDs, symbolic model checking fair CTL (MC book p. 53-59, 68-71)
- Week 11, Tuesday 1.6.10: Fair CTL continued, examples, counter examples and witnesses, mu-calculus
(MC book p. 71-75, 97-99)
- Week 12, Tuesday 8.6.10: Mu-calculus
(MC book p. 99-103)
- Week 13, Tuesday 15.6.10: Emerson-Lei algorithm, equivlences and preorders
(MC book p.103-108, 171-175)
- Week 14, Tuesday 22.6.10: Equivalences and preorders
(MC book p.176-180), examples and exam problems
- Week 15, Tuesday 29.6.10: Examples and exam problems, homeworks, questions
Results from the exam(s) and homeworks
|
Student ID
|
Exam points (<= 100)
|
HW points (*)(<= 11)
|
Project points (<= 25)
|
Mark (**)
|
Exam date
|
|
****057
|
94
|
11
|
25
|
1
|
6.7.2010
|
|
****642
|
86
|
11
|
25
|
1
|
6.7.2010
|
|
****270
|
76
|
9
|
25
|
2
|
22.7.2010
|
|
****614
|
74
|
3
|
22
|
2
|
22.7.2010
|
|
****594
|
73
|
11
|
22
|
2
|
22.7.2010
|
|
****203
|
73
|
2
|
22
|
2
|
10.8.2010
|
|
****112
|
72
|
11
|
25
|
2
|
6.7.2010
|
|
****510
|
50
|
-
|
20
|
4
|
22.7.2010
|
(*) There were 11 homeworks. Each delivered homework counts as one HW point.
(**) Total = Exam points + HW points + Project points.