|
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,
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:
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.