Logic Model Checking, Caltech 2018-19, Winter Term

Course Material CS 118, TThu, 1:00-2:25pm, 106 Annenberg

Logic Model Checking

An introduction to the theory and practice of logic model checking as an aid in the formal verification of concurrent or distributed systems, and specifically of 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 popular logic model checker Spin. Towards the end of the course we will also cover model-extraction techniques and the use of cloud computing in formal verification.

The course covers a broad range of fundamental computer science topics, including the use of hashing, search methods, graph theory, automata theory, non-determinism, omega-regular properties, concurrent algorithms, storage methods, Bloom filters, the use of logic, user interfaces, language design, parsers, etc.

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. If you're registered for the class, you'll receive an invitation to join.

Assignments:
A fair amount of self-paced work with the Spin and Buzz model checkers and related tools (e.g., Tau and iSpin, and possibly also Modex), is expected. Grading is based on in-class quizzes and 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 feasible and tractable.

• All assignments require individual work.
• You may suggest a challenging formal verification task to replace any assignment.
  Similarly, you may suggest to design and build non-trivial components of alternative verification systems.
• The first lecture is Tuesday January 8; the last will be Tuesday March 12.
• Additional materials are posted on Piazza.

Lectures

• You are expected to attend all lectures, ask questions, start discussions, suggest problems.
• Part of the course credit is based on your class participation.

Recommended Preparation

• Install the most recent version of Spin on your system (6.4.9).
  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 instructions.

Instructor

• Gerard J. Holzmann, gholzmann [at] acm.org, homepage

Teaching Assistant

• Tung M. Phan, tmphan [at] caltech.edu.

Course Website

• http://spinroot.com/cs118/

Background material

• Dijkstra's paper on guarded commands
• Hoare's paper on CSP
• Amir Pnueli's 1977 paper on temporal logic and model checking
• How many CPUs are there in a Mercedes S-class car? (50!)
• NIST report on economic impact of faulty software
• Standish survey of software projects
• Model Checking overview by Stephan Merz
• Wiki entry on formal verification
• IEEE Spectrum: Why software fails
• Wired: History's Worst Software Bugs
• CNN/Money: Prius hybrids dogged by software
• Computerworld: Buggy software costs $60B annually
• Embedded.com: Automotive industry software bugs
• ACM Paper on out-of-order execution on modern processors
• Spin model based on this paper, showing the bug in Peterson's mutual exclusion algorithm when executed on a modern processor
• Truth a thought provoking editorial published in 2008 in the Notices of the AMS.

Course Textbook

• The Spin Model Checker: Primer and Reference Manual.
  Gerard Holzmann. Addison-Wesley, 2004.

Optional:

• 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.
• Model Checking,
  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:

• Algorithms for Mutual Exclusion, Michel Raynal, MIT Press, 1986.
• Distributed Algorithms and Protocols, Michel Raynal, Wiley&Sons, 1988.
• Topics in Distributed Algorithms, Gerard Tel, Cambridge Univ. Press, 1991.