TTh 330-450 Tech M120

Prof. Hai Zhou

haizhou AT northwestern DOT edu

L461 Tech Institute

(847) 491-4155

Office Hours: T 2-330 or by appointment

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.

L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley. 2003.Reference: E. M. Clarke Jr., O. Grumberg, and D. A. Peled, "Model Checking", The MIT Press, Cambridge, London. 1999.

- 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.
- E. W. Dijkstra, The calculus of boolean structures (Part 0), EWD1001.
- E. W. Dijkstra, The calculus of boolean structures (Part 1), EWD1002.
- 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.
- C. A. R. Hoare, An Axiomatic Basis for Computer Programming. Communications of the ACM, vol. 12, no. 10, Oct. 1969.
- 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.
- 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.
- B. Alpern and F. B. Schneider, Recognizing Safety and Liveness. Distributed Computing, Vol 2(3), pp. 117-126, 1987.
- 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.
- K. McMillan's tutorial on verification: introduction, model checking 1, model checking 2, symbolic model checking

Grading: 10% class participation 90% homeworks and projects

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

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

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

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

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

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

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

Week 8Composing and decomposing systems Reading: ch. 10

Week 9-10Distributed 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.