Logic Model Checking, Caltech 2015, Winter Term
Course Material CS 118, TThu, 1:00-2:25pm, 314 Annenberg
Logic Model Checking
This course offers an introduction to the theory and practice of logic model
checking as an aid in the formal verification of concurrent and multi-threaded
software systems. The specific focus is on the automata-theoretic verification
method, on the formalization of properties in linear temporal logic, and the use
of the Spin model checker.
The course also covers automated model-extraction and
swarm-based verification techniques using grid networks,
the cloud, and standard multi-core machines.
At the end of the course you should have a good fundamental insight into the
theory of logic model checking based on automata-theoretic verification, and the
direction in which the research in this area is evolving. At that point you should be able
to handle significant real-world software verification problems, especially of
systems involving concurrency.
There are seven take-home assignment, roughly one per week, and especially
in the beginning a fair amount of self-paced work with Spin is expected.
Some of the assignments will require significant effort, formalizing
problems and finding abstractions to make verification tractable.
The first five assignments each count for 10% of the final grade;
the last two assignments each count for 25%.
All assignments require individual work (there are no team assignments).
Don't plan on being able to to complete assignments
in a single late-night session, the day before it is due.
You are allowed to suggest a challenging verification task yourself,
to replace the final two assignments
(prior instructor approval required of course).
The maximum score for each assignment is 100 points.
If you send in your solution past the due date/time,
10 points are deducted for every 24 hour period
or part thereof. (I.e., at the start of the 10th day late, zero points will remain.)
A letter grade for the course is derived from the following ranges for the
weighted average score on all assignments:
95 - 100 = A+
85 - 94 = A
80 - 84 = B+
70 - 80 = B
65 - 69 = C+
55 - 64 = C
Examples of assignments and small model checking applications will be discussed
during each lecture, so you are strongly encouraged to
attend in person. It is possible that some assignments are done only
in class this year, which can gain you additional credits towards the final grade.
At the start of the course you are expected to download and
install the latest version of Spin model checker
on your preferred system (linux recommended).
Throughout the course you are further expected to take the initiative to
experiment on your own with the tool to learn in more detail about
concepts explained in the lectures, and to ask questions based on these experiments.
You are strongly encouraged to try small
examples to develop and fine-tune your model building, abstraction, and verification skills,
and to develop insight in the verification strategies that are typically used with logic model
checkers. Self-paced work is expected throughout the course.
- You are strongly encouraged to attend all the lectures, to ask questions, to start discussions.
Assignments and Exercises
- All assignments and exercises will be posted here, with their due dates (but no lecture notes).
- Solutions to the assignments must be send in by the due date, to count for the final grade.
The recommended excercises are for you to gain experience with key concepts and
need not be handed in.
- Solutions to the assignments and exercises are discussed only in class, once all
responses have been received.
by January 6, 2015:
by January 13, 2015:
- Install the most recent Spin version 6.4 on your system.
Download the full source
distribution, compile it (you must have gcc or equivalent on you system) and
install it on your system. If using a Windows PC, make sure you can compile the code
correctly (see make_pc in the source directory from the distribution). Try
the test-cases from the Spin/Test directory.
- Install the latest version of the Spin GUI called iSpin.
(To use the GIUI, you must also have a recent version of
tcl/tk and graphiz/dot installed on your system).
If needed, follow the
by February 3, 2015:
- Study Chapters 1-3 of the course textbook.
- Complete the exercises 1a through 1h from:
- Study Chapters 4-5 and Appendix B.
- Take a look at the first three links below under Background material.
Will be posted here.
- Gerard Holzmann, gholzmann [at] acm.org
Principles of Spin,
Moti Ben-Ari, Springer Verlag, Jan. 2008.
Principles of Model Checking,
Cristel Baier, Joost-Pieter Katoen, Kim Larsen, MIT Press, May 2008.
Principles of concurrent and Distributed Programming,
Moti Ben-Ari, Addison-Wesley, 2006, 2nd Edition, based on Spin.
Ed Clarke, Orna Grumberg, and Doron Peled. MIT Press, 1999.
Systems and Software Verification: Model-Checking Techniques and Tools,
Beatrice Berard, Michel Bidoit, Alain Finkel, et al, Springer Verlag, 2001.
Logic in Computer Science: Modelling and Reasoning about Systems,
Michael Huth and Mark Ryan, Cambridge Univ. Press, 1999.
Introduction to Automata Theory, Languages, and Computation (2nd Edition),
John Hopcroft, Rajeev Motwani, Jeff Ullman, Addison-Wesley, 2000.
Verification of reactive systems,
Klaus Schneider, Springer-Verlag 2004.
Formale Modelle der Softwareentwicklung (in German),
Stephan Kleuker, Vieweg-Teubner Verlag, 2009.
Covering Spin, Uppaal, and Petri Nets.
For more on mutual exclusion algorithms, and design of distributed algorithms
in general, consider also: