EECS 356 Introduction to Formal Specification and Verification

Time & Place

TTh 330-450 Tech M120

Instructor

Prof. Hai Zhou
haizhou AT northwestern DOT edu
L461 Tech Institute
(847) 491-4155
Office Hours: T 2-330 or by appointment

Overview

The biggest challenge in digital system design is to maintain the complexity at a manageable level. Considering the behavior of a system case by case is no longer working, either in design or verification. Formal techniques treat a design as a mathematical object and establish its behavior from its structure through mathematical reasoning--that is, proofs. In this course, we will study a selected set of formal techniques and their applications in digital system specification, design, and verification.

Required Text

L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley. 2003.

L. Lamport's TLA Web Page

Reference: E. M. Clarke Jr., O. Grumberg, and D. A. Peled, "Model Checking", The MIT Press, Cambridge, London. 1999.

Reading List

  1. L. Lamport, Verification and Specification of Concurrent Programs. "A Decade of Concurrency: Reflections and Perspectives", J. W. de Bakker, W.-P. de Roever, and G. Rozenberg editors. Lecture Notes in Computer Science, number 803, Springer-Verlag. June, 1993. pp. 347-374.
  2. E. W. Dijkstra, The calculus of boolean structures (Part 0), EWD1001.
  3. E. W. Dijkstra, The calculus of boolean structures (Part 1), EWD1002.
  4. R. W. Floyd, Assigning Meanings to Programs. In J. T. Schwartz (ed.), "Mathematical Aspects of Computer Science", vol. XIX of Proceeding of Symposia in Applied Mathematics. Providence: American Mathematical Society, 1967.
  5. C. A. R. Hoare, An Axiomatic Basis for Computer Programming. Communications of the ACM, vol. 12, no. 10, Oct. 1969.
  6. R. Joshi, L. Lamport, J. Matthews, S. Tasiran, M. Tuttle, and Y. Yu, Checking Cache-Coherence Protocols with TLA+. Formal Methods in System Design, 22(2), March 2003. pp. 125-131.
  7. J. E. Johnson, D. E. Langworthy, L. Lamport, and F. H. Vogt, Formal Specification of a Web Services Protocol. In the First Interantional Workshop on Web Services and Formal Methods (WS-FM 2004), Pisa, Italy. The TLA+ specification can be found here.
  8. B. Alpern and F. B. Schneider, Recognizing Safety and Liveness. Distributed Computing, Vol 2(3), pp. 117-126, 1987.
  9. Chapters on "Temporal Logic" and "Model Checking" in E. M. Clarke Jr., O. Grumberg, and D. A. Peled, "Model Checking", The MIT Press, Cambridge, London. 1999.
  10. K. McMillan's tutorial on verification: introduction, model checking 1, model checking 2, symbolic model checking

Policies

Grading: 10% class participation  90% homeworks and projects

Homeworks

  • Homework 0 (out 1/8 due 1/10): bio and background
  • Homework 1 (out 1/15 due 1/22): simple math and specs
  • Homework 2 (out 1/31 due 2/7): temporal logic and proofs
  • Project (out 2/5): instructions
  • Reading Assignment: Existence of Refinement Mappings
  • Homework 3 (out 2/19 due 3/5): model checking
  • Reading Assignment: Real Time is Really Simple
  • Homework 4 (out 3/5 due 3/14): realtime and composite specs
  • Reading Assignment: Self-stabilization in spite of distributed control
  • Reading Assignment: The Part-Time Parliament
  • Lecture schedule

    Week 1 Euclid's algorithm and TLA specs Reading: hyperbook 2,3

    Week 2 Asynchronous interface specification and TLATeX typesetter Reaching: ch. 3, 13

    Week 3 Mutual Exclusion and TLA Proofs Reading: hyperbook ch.5

    Week 4 Temporal logic: safety and liveness properties, TLC Reading: ch. 8

    Week 5-6 Model checking and TLC Reading: handouts and ch. 14

    Week 7 Specification and verification of real time systems Reading: ch. 9

    Week 8 Composing and decomposing systems Reading: ch. 10

    Week 9-10 Distributed systems and algorithms Reading: handouts

    Please check back often to this page (www.eecs.northwestern.edu/~haizhou/356) for updates and course material down-loading.