TTh 330-450 Tech M120
Prof. Hai Zhou
haizhou AT northwestern DOT edu
L461 Tech Institute
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.
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.
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 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.