Logic Model Checking, Caltech 2017, Winter Term
Course Material CS 118, TThu, 1:00-2:25pm, 106 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 systems
and multi-threaded software.
The focus is on the automata-theoretic verification
method, the formalization of properties in linear temporal logic, and the use
of the widely used logic model checker Spin.
The course also covers model-extraction and
swarm-based verification techniques using cloud computing.
At the end of the course you should have a good 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 will also be able to tackle complex real-world verification problems for
software systems involving concurrency.
Course materials, including assignments and additional tools, will be posted on Piazza.
A fair amount of self-paced work
with the Spin model checker is expected.
Grading is based on take-home assignments, some of which
require the correct formalization of problem statements and
the identification of logic abstractions that can render tool-based
formal verification tractable.
There will be seven assignments (roughly one per week).
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.
You may suggest a challenging formal verification task
to replace one of the final two assignments, with approval from the instructor.
Similarly, you may suggest to build a non-trivial component of an alternative
prototype verification system that will be provided.
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 that your submission is late.
This means that at the start of the 10th day late, zero points 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 model checking applications are discussed
in class, so you are strongly encouraged to attend all lectures.
It is possible that some assignments will be done
in class, which can gain you additional credits towards the final grade.
Throughout the course you are encouraged to
experiment on your own to learn in more detail about
concepts covered in the lectures, and to ask questions based on these experiments.
Fine-tune your model building, abstraction, and verification skills by
creating lots of small example verification models.
Self-paced work is expected throughout the course.
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 or linux-compatible systems are recommended),
plus some additional course-specific tools
(such as tau and buzz).
We will discuss the formal specification language in the early lectures,
but you are encouraged to look at examples, read the textbook, and
to become familiar with the online manual pages at:
- You are encouraged to attend all lectures, ask questions, and start discussions.
- The first lecture was Thursday January 5; the last will be Tuesday March 9.
- Excerpts from some lectures are posted on Piazza (send an email if you're
registed but didn't receive an invite yet)
- Install the most recent version of Spin on your system (6.4.6).
Download the full source distribution,
compile it (requires gcc or equivalent) and
install it on your system. Make sure you can compile the code correctly. Try
the test-cases from the Spin/Test directory to make sure.
- Download and install iSpin, the Spin GUI.
(To use the GUI, you must have a current version of
tcl/tk and graphiz/dot installed on your system).
In case of problems, follow the online
- Optionally: install the Tau tool, available from spinroot homepage.
All assignments are posted on the Piazza website.
- by January 17, 2017:
- Read at least upto Chapter 3 in the course textbook.
- Complete exercises 1a through 1h from:
(self-paced; no need to submit)
- Assignment 1, was due no later than noon Jan 19
- Assignment 2. is posted Jan 19, and due noon Jan 26
- Assignment 3. is posted Jan 26, and due noon Feb 2
- Assignment 4. is posted Feb 2, and due noon Feb 9
- Assignment 5. is posted Feb 9, and due noon Feb 16
- Assignment 6. is posted Feb 16, and due noon Feb 24
- Assignment 7. is posted Feb 28, and due noon March 10
Solutions to assignments will be discussed in class, once all
solutions have been received.
They will not be posted online.
- Gerard Holzmann, gholzmann [at] acm.org
- Sumanth Dathathri
office hours Tuesdays 6-8pm, SFL 229, on weeks when homework is due.
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:
The following course is recommended as either a prelude to or follow-up to CS118:
- CS116, Reasoning about program correctness.
Lecturer: Rajeev Joshi (JPL/LaRS).