Formal Methods in System Design, Spring 2007
School of Computing, University of Utah
Course Number: CPSC 6110
T,H 2:00 PM-3:20 PM --- MEB 1225

Instructor: Prof. Ganesh Gopalakrishnan

    This index [.ps] [.pdf] [.tex]    
    Fall'07 Academic Calendar --- ACS    




LINKS TO HANDOUTS (Section 5)

1  Overview

Programmable computing systems (``computers'') are employed virtually everywhere. Just about any device that has some electricity involved in its operation can (and often does) employ a programmable computer that runs software. Just to list a few specific examples, they include consumer electronic goods such as cell phones and cameras, reliability critical systems such as microprocessor cache coherence controllers and medical electronic devices, very expensive artifacts such as supercomputing systems and satellites, and devices intended for mass deployment such as smart cards and smart sensors.

Computers must work correctly: their failure to do so -- due to bugs -- can lead to expensive field repairs, destruction of property, product recalls, or even loss of life, as several real-world experiences have unfortunately shown. However, characterizing computers and their operation solely in terms of ``bugs'' is taking a very simplistic view. Most computing artifacts (hardware and software) possess fairly complex behaviors. The degree of precision with which the behaviors of individual components is described, the intuitiveness of such descriptions, the degree of composability of their external interfaces, and the predictability of such compositions -- all help determine how ``well engineered'' a computing system is perceived to be.

To help make the above points more forcefully, consider the progress made in the design of missiles. The ``power'' of missiles is largely characterized by the precision of their strike. The more predictable the missile is, the more ``lethal'' it is. The same is true of engineered components: the more reliable and precision machined it is, the more amenable they are to building high reliability systems. In this sense, formal methods play two fundamentally important roles. (i) as commonly understood, they help eliminate blatant errors in either the specifications or the implementations of computers. (ii) much more fundamentally, they help enhance the precision with which a computer or a computing component (a computing ``brick'') is described -- whether it be in terms of its energy needs or all its usage modes as well as usage restrictions.

It must also be clear that precise descriptions by themselves do not guarantee either ease of use or reduced propensity to misuse. Rather, each formally described system ought to be ``well rounded'' in the sense of being easy to use and orthogonal in terms of its behavior. The more precisely characterized and the more well-rounded the description of a component is, the more it helps build up towards more reliable large-scale computing systems.

The adoption of formal methods forces one to economize on the concepts employed, as well as seek consistency as well as relationships among various concepts. If these concepts are translated back into a combination of English as well as semi-formal notations, one often obtains far more useful documentation than one obtains with an approach that relies solely on informal reasoning.

The discipline of formal methods offers techniques to write clear formal specifications, as well as tools to validate specifications in terms of detecting and eliminating internal contradictions or omissions. Formal specifications themselves may be furnished in terms of a list of properties or in terms of simple (and hence trusted) reference implementations. Often multiple specifications are created and reconciled against each other.

The discipline of formal methods also encompass tools to verify actual implementations against formal specifications. Methods to locate bugs in computers constitutes well over 70% of their development cost. Tools based on formal methods will be widely used even if they report the existence of bugs which other ``semi-formal tools'' fail to report. Clearly they are much more useful if they provide an error trace. They will be still more useful if they can help locate as well as correct the errors. Almost all these problems are, in a formal sense, known to be formally undecidable; yet, formal methods deliver in practice because they seek to evolve automatable approaches that work for specific problem domains.

This course is designed to help you learn about the role of formal methods in specifying and verifying computing systems. The selection of topics in this class is guided by our goal of providing you with some knowledge that you can cherish as well as employ long-term. We will include a selection of classical topics, as well as a discussion of modern directions being pursued. The Programming Languages and Systems (``AMPS'') seminar will offer us opportunities to read and discuss modern papers in model checking.

This course has a heavy project emphasis, and you will be able to learn several topics in depth through your projects. You should ideally be able to publish a `decent' workshop paper (of 10-12 pages) based on your project.

Being tied so closely to commercial aspects, there is an inevitable tussle between the cost of applying formal methods and the risk of not doing so. In many instances, the cost of applying formal methods is still prohibitive; in these instances, continued research will help mitigate the costs. In many instances, however, the cost is exaggerated and based only on short-sighted measures. While these considerations are important, we will not have time to discuss these issues in depth.

2  Software

This course will involve the use of the SPIN model checker (www.spinroot.com), the Murphi model checker (www.cs.utah.edu/formal_verification) and the NuSMV model checker (nusmv.irst.itc.it). We are expecting that the students can download and install these tools. Additional tools will, most likely, be involved.

3  Books, References

The following books are highly recommended for the reasons indicated. Papers will be heavily used, as will our class notes.
  1. ``The Spin Book.''
    The SPIN Model Checker -- by Holzmann -- Addison-Wesley, 2004. We will use this a lot to study SPIN as well as model checking principles. So if you wish, you may buy a copy (e.g., Amazon has many used copies.) I won't be able to supply xeroxes (beyond, say, the first lecture or two, to allow you time to buy a copy if you wish).

  2. ``The Clarke book.''
    Model Checking -- by Clarke, Grumberg, Peled -- MIT Press, 1999. We will use this a lot to study the principles of model checking.

  3. ``My book.''
    Computation Engineering: Applied Automata Theory, and Logic -- by Gopalakrishnan -- Springer, 2006. (Amazon link) We will refer to this book a lot for the basics, including automata theory, logic, and model checking basics.

4  Topics

The topics we hope to cover are listed below. Students will be required to propose lectures from these (or even outside of these) topics, for example where the lecture plans indicate ``tbd''. The students will also be required to give some of the(se) lectures. Our current lecture plans are given in Section 5 (subject to change/refinement).
  1. Overview of finite state model checking
    1. Model checking using SPIN (My book, SPIN notes)
    2. Partial Order Reduction (Clarke book)
    3. Recent paper(s) on partial order reduction
    4. Model checking using Murphi (Murphi notes)
    5. Symmetry Reduction (Papers)
    6. Recent paper(s) on symmetry reduction


  2. Temporal Logics
    1. LTL, CTL (My book, Clarke)
    2. CTL*, mu-Calculus (Clarke)
    3. Safety, Liveness, Fairness
    4. Simulation, Bisimulation (Papers, Clarke)
    5. Equivalences and Preorders (Papers, Clarke)


  3. Symbolic model checking
    1. CTL (My book, Clarke, Papers)
    2. LTL (My book, Clarke, Papers)
    3. Bounded Model Checking (Papers)
    4. SAT, K-induction, and related topics (Papers)


  4. Program Logics, Decision Procedures
    1. Floyd/Hoare Logic (Gordon's book, Software)
    2. Use of uninterpreted functions in modeling (Uclid examples)
    3. Satisfiability Modulo Theories (Barrett's Dissertation, CVC)
    4. Applications in Program Verification/Testing (Papers, including by Engler)


  5. Reasoning About Pipelined Concurrency
    1. Refinement based verification
    2. Pipelined Processor Correctness Proofs (Papers by Burch/Dill, Aagaard et.al., Day, and others, and dissertations by Hosabettu, Srinivasan, etc.)


  6. Abstraction and Refinement Methods, Compositional Methods, Assume/Guarantee Methods (all discussed through specific papers)

  7. Project selection; student paper presentations concurrently

  8. Final project presentations

5  Lecture Plans

Week 1 -- 8/21 and 8/23:


General intro, Ch 2-3 from the SPIN book, Leader Election from the Clarke book (also in the SPIN distribution) to be examined using SPIN.

Week 2 -- 8/28 and 8/30:


Week 3 -- 9/4 and 9/6:


Automata and Logic from the SPIN book. CTL and LTL from my book. Exercises from my book and other sources to reinforce CTL and LTL. Lecture slides are in

lec5-6110-9-4-07.pdf

Week 4 -- 9/11 and 9/13:


More on Temporal Logics: CTL, LTL, CTL*. Then process equivalences. Mostly from the Clarke book. I've also kept lecture slides online (updated from version handed out in class), in lec7-6110-9-11-07.pdf.

Finally, there are many useful models of counters kept ready for NuSMV experimentation (torture?).

A README file hopefully explains some of this.

The Clarke and Draghicescu paper is available from THIS URL that has ALL of Prof. Clarke's papers. We will discuss this paper in class during Lecture 8.

Week 5 -- 9/18 and 9/20:
] Ended up presenting two things through hand-written notes: Assignment and some other references are online.

Week 6 -- 9/25 and 9/27:
Partial Order Reduction; Intro to Murphi.

Week 7 -- 10/2 and 10/4:
Lecture by Xiaofang Chen on 10/2, presenting her Assume/Guarantee method to verify large protocols. Murphi examples and problems involving the use of Murphi to be provided. Assign problems to be worked out by the class over the Fall Break.

We will study Floyd/Hoare Logic and Subgoal induction in detail.

We'll finish Murphi on 10/4, briefly covering some Murphi-related algorithms: (i) symmetry, (ii) hash compaction, (iii) parallel and distributed Murphi (Eddy Murphi). You will explore (iii) in detail through asg7.

See README for details.

See this URL for a free copy of Michael Gordon's entire book. This book describes the Hoare Logic prover. Michael Gordon' book.

Fall break
Week 8 -- 10/16:


Week 9 -- 10/23 and 10/25:


Week 9 -- 10/25:
Project Meetings: Each will consist of eight 20-minute meetings (with 10 mins rest for me after each meeting) held between 1pm and 5pm, beginning at the following times (sign-ups so far are also shown):

Week 10 -- 10/30:
Study of the Satabs tool.

Week 10 -- 11/1:
Study Das's work on Predicate Abstraction.

Week 11 -- 11/6:
Assignment 10 (LAST ONE) on Pred Abs. Please finish all Asgs by 11/15.

Week 11 -- 11/8:
Project Meetings

Week 12 -- 11/13:
Lecture by Yu Yang on Interpolation in verification. (Ganesh away.)

Week 12 -- 11/15:
Project Meetings

Week 13 -- 11/21:
Boolean satisfiability

Week 14 -- 11/27:
Simulation, Bisimulation, Safety, Liveness

Week 14 -- 11/29:
Decision procedures (Satisfiability modulo theories or SMT)

Week 15 (Last Week of Classes) 12/4 and 12/6:


NOTES for 12/4/07

12/10:
Project presentations

6  Project Offerings

Students engaged in research are requested not to entirely double dip. They are strongly encouraged to select a class project that is very helpful and additive to their research, but ``different enough'' (e.g. ``30% new'') from what they are already working on for research. All this can be negotiated.
  1. Design of new cache coherence protocols, and verification of these protocols (interleaving models) using Murphi and assume/guarantee methods.

  2. Design of cache coherence protocol hardware implementations, and verification thereof.

  3. Porting Murphi to a thread-parallel language/library such as OpenMP

  4. Projects on Hardware Transaction Memories (in collaboration with Prof. Balasubramonian)

  5. Projects on symmetry reduction / parameterized reasoning applied to message passing (e.g. MPI) and shared memory thread (e.g. OpenMP/PThreads) programs

  6. Synthesis of message passing (e.g. MPI) and shared memory thread (e.g. OpenMP or PThreads) programs that are ``correct by construction'' (less post-synthesis verification involved).

  7. Improvements in the practical usability of partial order reduction.

  8. Projects on weak memory models (hardware, language level, with/without transactions, compilation oriented, verification oriented, litmus-testing oriented)

  9. Verifying programs/compilers under weak memory semantics.

  10. Novel combinations of explicit state (enumerative) and implicit state (symbolic) verification methods.

  11. Novel combinations of static and dynamic analysis methods.

  12. Novel combinations of static analysis and model checking.

7  Background Assumed

Ideally, I require a background very similar to that imparted in my recently concluded class CS 6100. This version of 6100 covered not only ``Classical Automata Theory and Computability,'' but also examined first order logic, Binary Decision Diagrams, Boolean SAT, and simple ideas from symbolic and explicit-state model checking.

For those not possessing this very background, I still require a working knowledge of classical automata theory. If you possess an elementary knowledge of first-order logic, the course will be quite smooth; if you don't, we will help you acquire this background.

Those who have done automata theory but not first order logic, but instead have programmed in logic programming languages and/or higher order functional programming languages may also possess the required background.

Finally one who is not scared by formal concepts (and wants to learn them), and has a very good programming background (both sequential and concurrent) is also welcome.

In all cases, there will be independent reading that is required in order to catch up. Help will be offered outside of lecture time, if need be.

As usual, please contact me if unsure whether your background is good enough for this class.

8  Grading

There will be plenty of homeworks assigned early on. They will be graded - some through the help of the class. The homeworks will taper off as the semester advances. Once the projects are underway, emphasis will shift towards 1-1 meetings in lieu of homeworks and grading. The final course letter grade depends on the degree of learning you achieved and demonstrated, and especially the quality of your project.

9  Calendar


        August              September              October               November              December
 Su Mo Tu We Th Fr Sa  Su Mo Tu We Th Fr Sa  Su Mo Tu We Th Fr Sa  Su Mo Tu We Th Fr Sa  Su Mo Tu We Th Fr Sa
           1  2  3  4                     1      1  2  3  4  5  6               1  2  3                     1
  5  6  7  8  9 10 11   2  3  4  5  6  7  8   7 fb  .  .  . FB 13   4  5  6  7  8  9 10   2  3  4  5  LL CE 
 12 13 14 15 16 17 18   9 10 11 12 13 14 15  14 15 16 17 18 19 20  fc  .  . FC 15 16 17   
 19 20 FL 22 23 24 25  16 17 18 19 20 21 22  21 22 23 24 25 26 27  18 19 20 21 tg TG 24  
 26 27 MS 29 30 31     23 24 25 26 27 28 29  28 29 30 31           25 26 27 28 29 30     
                       30                                                                

FL = First lecture; LL = Last lecture; CE = Classes End; fb/FB = Fall Break; tg/TG = Thanksgiving
MS = Microsoft visit; fc/FC = FMCAD trip

10  ADA Statement

The University of Utah seeks to provide equal access to its programs, services and activities for people with disabilities. If you will need accommodations in the class, reasonable prior notice needs to be given to the Center for Disability Services, 162 Union Building, 581-5020 (V/TDD). CDS will work with you and the instructor to make arrangements for accommodations.

This document was translated from LATEX by HEVEA.