Comp. Sci. 613 (691P) Model Checking Fall, 2007

Instructor: Neil Immerman

Office Hours: Monday, 2:00 to 3:30, and by appointment,

What is this course about? This will be an in-depth, hands-on introduction to the theory and practice of model checking. We will learn how to check that hardware and software satisfy correctness conditions specified by temporal logic, first-order logic, or finite automata. Topics include: fast introduction and review of first-order and temporal logic, model checking temporal logic, symbolic model checking using binary decision diagrams, bounded model checking using SAT solvers: NuSMV, automata theoretic model checking: SPIN, Abstraction: dealing with state explosion by making the models smaller, Real-time modules and timing verification. We will also make use of some software model checking tools such as SPIN, BLAST and TVLA.

Meeting Times: Tues, Thurs, 2:30 - 3:45, CMPS 374, with the first meeting on Thursday Sept. 6. Note that the course was originally scheduled for Mon, Wed: 10:35 - 11:50, but several students had a conflcit with CMPSCI 683, which also meets at that time. If you want to take this course but can't make the new time, please contact me as soon as possible.

Text: Systems and Software Verification by B. Bérard and 6.5 other authors. I just chose this recently and hence did not order it from a bookstore. It's not too expensive and has the advantages in my opinion that it provides the basics, its notation is reasonably clear, and it is not hard to read. This will be a good base to build upon.

Please buy the text and read the first chapter, which should be easy for you. My plan is to cover this book, enriched by papers, in the first half of the class, and then move on to slightly more advanced topics, depending on the interests of the class members.

Requirements: problem sets, in class midterm, and final project. The final project --- which should be discussed with the instructor by the midterm --- will be an in class presentation accompanied by a short paper. Topics could range from the following: an application of formal verification, a case study to compare different tools or methods, an implementation and testing of an algorithm, an independent study of a related topic.

Prerequisites: Mathematical maturity at the level of an A in Comp Sci 250 is necessary. Students will also need to have knowledge of algorithms and automata theory at the level of CMPSCI 311 and CMPSCI 401. That said, I am hoping that students will have completed at least one of 601 and 611. If you have a question whether your background is sufficient please come talk with me.

What is Model Checking? For a long time, the area of formal methods had a reputation of claiming more than it could deliver. The promise of proving large programs and systems correct was held out for decades as a technology that was right around the corner. Model checking is a modest approach to formal methods. This modesty is misleading; model checking is practical and useful. Many hardware design companies, including Intel, have adopted model checking as part of their basic design method

The idea is simple. When we design a program, distributed protocol, or circuit, we do so in a formal language. This might be a circuit design language such as VHDL or Verilog, or a system specification language such as State Charts or Heitmeyer's SCR, or Alur and Henzinger's Reactive modules, or even in a programming language such as Java.

Such a formal design determines a logical structure,

K = < S, p1, … , pk, R >

called a Kripke structure or transition system. S consists of the set of possible global states of the design, the set of all possible gate values for the circuit, or all possible assignments of values to the variables of a program, or all possible assignments of states to each processor in the distributed protocol. Binary relation R is the next move relation: R(s,s') means that the move from s to s' is a possible atomic transition of the circuit or program. Unary relations p1, … , pk express properties of the global states, for example, being an initial state, being an accepting state, or that a particular variable has a special value. The size of S is often exponential in the size of the design. This phenomenon is typically referred to as the state explosion problem.

Once we have our formal design, a representation of the transition system can be automatically generated. We may now wish to write some simple correctness conditions in a formal language. For example, we might want to express the following:

  1. If the Restart button is pressed, we eventually restart.
  2. Doors are not opened between stations.
  3. Division is performed correctly.
  4. The motor is not turned on during maintenance.
These conditions express the fact that (1) if we press the Restart button on a personal computer it will eventually restart --- without our having to unplug it and plug it in again; (2) the subway train controller meets some simple safety conditions; (3) Intel's new processor does its arithmetic correctly; and (4) the mixer in a nuclear waste storage container (which is designed to keep its contents mixed and thus less volatile) cannot turn on (and thus cause injury) during maintenance.

Now that we have formally expressed our design and our statement concerning its behavior, we can simply press a button and be told whether or not K ⊨ ϕ, that is, does the design satisfy the desired property?

This is the model checking problem: given K and ϕ, test whether K satisfies ϕ. Model checkers are being hailed as great debugging aides. We can write a simple property that our system should satisfy and press the button. If it does not satisfy the property then we will be told so. Typical model checking programs will present a counter-example run of the system, i.e., they produce the explicit bug. If the model does satisfy the property, then we will be told so. Note that this is better than just not finding a bug. Our model checker has automatically proved that our design has a certain desirable property.

Model Checking has already succeeded in finding many bugs in circuit designs that escaped less formal debugging and testing methods. The potential for model checking goes well beyond debugging circuit designs. Recently, significant progress has also been made in model checking of software.

As a user designs a circuit, program, web page, lecture, book, course, etc., the system on which it is designed can have a formal model of what is being constructed. The user can ask if the design will have a certain simple property. The system will answer, ``no, and here is a bug'', or ``yes''. If the answer is yes, then that can be something that this user or even other users can depend upon and build upon. Furthermore, the system could ask if the property should be checked for dynamically, i.e., the system could issue a warning if a later change in the design caused the desired property to be violated. In fact, there is an enormous potential here for rational, computer-aided design, verification, and maintenance. To accomplish this, it is necessary to maintain a formal model and to keep the query language simple.