CIS 673: Computer-Aided Verification, Fall 2006
Class: Mon Wed 10.30--12.00, Towne 303
Office hours: by appointment
Introduction
How can a designer check that the system (s)he has designed works
correctly? Can an airline control system fail in a critical way when
a piece of hardware fails? Will a cache coherence protocol continue
to work correctly when an extra processor is added? Today, designers
attempt to answer such questions using simulation over selected
sample cases. As reactive systems become more complex and pervasive,
simulation-based techniques are not sufficient to assure desired
reliability. Model checking and related computer-aided verification
techniques are emerging as practical alternatives to simulation
for debugging complex systems. These methods allow the designer
to verify that a mathematical model of a system satisfies its
abstract logical specification. This approach has been most effective
in analysis of control-intensive hardware components, and is rapidly
becoming an integral part of the design cycle in companies like Intel and Microsoft.
Prerequisites
The course requires basic knowledge of algorithms, data structures,
automata theory, computational complexity, and
propositional logic (CIS 502, CIS 511, or equivalent).
Knowledge of operating systems, communication protocols,
and hardware is useful.
The course requires mathematical maturity, and is appropriate
for graduate students who wish to pursue research in
formal methods or related areas.
If you need more information to decide, contact the instructor.
Overview
The course introduces the theory and practice of formal methods
for the design and analysis of concurrent and embedded systems.
The emphasis is on the underlying logical and automata-theoretic
concepts, the algorithmic solutions, and heuristics to cope with
the high computational complexity.
Topics include
- Models and semantics of reactive systems:
states vs. events, nondeterminism vs. concurrency, synchrony
vs. asynchrony, safety vs. liveness, refinement preorders,
real-time and hybrid systems, open systems.
- Verification algorithms:
temporal logic model checking, theory of
omega automata, games, minimization.
- Verification techniques:
symbolic model checking, on-the-fly model
checking, state space reduction methods, compositional and
hierarchical reasoning, abstraction and refinement.
Model Checking Tools
Reading
The course will use the draft of a textbook
titled Computer-aided verification by Alur & Henzinger, 1999.
Following books are recommended for additional reading
- Model Checking, Clarke, Grumberg, and Peled, MIT Press, 2000.
- Design and Validation of Computer Protocols, G.J. Holzmann.
Prentice-Hall, 1991
-
Symbolic model checking: an approach to the state explosion problem,
K.L. McMillan, Kluwer Academic Publishers, 1993
- The temporal logic of reactive and concurrent systems: Specification,
Z. Manna and A. Pnueli, Springer-Verlag, 1991
Grading
There will be periodic homework assignments consisting of
theoretical problems and experimentation with model checking tools.
There will be no exams.
A key component of the evaluation will be the class project.
Tentative Schedule
- 9/6: Introduction
- 9/11,13: Modeling language: reactive modules
- 9/18: Invariant verification
- 9/20,25: Symbolic search, SAT and BDDs
- 9/27: Stable partitions, Symmetries, and Minimization
- 10/2,4,9: Safe temporal logic STL, model checking, distinguishing and expressive power
- 10/11,16,18: Trace semantics, compositionality, asssume-guarantee, simulation relations, homomorphisms
- 10/23: Fall Break
- 10/25: Guest lecture
- 10/30: Omega-languages, safety versus liveness
- 11/1: Fair modules
- 11/6,8: Searching for fair cycles and response verification
- 11/13: CTL, Mu-calculus, and Symbolic model checking
- 11/15, 20: Theory of omega-regular languages, Linear temporal logic LTL
- 11/22: Games and synthesis
- 11/27: Thanksgiving break
- 11/29, 12/4: Abstraction, refinement and software model checking
- 12/6: Model checking structured programs
- Week of 12/11: Project presentations
Lectures
- Lecture 1: Introduction, Sept 6
- Lecture 2: Modeling, Sept 11
- Lecture 3: Modeling, Sept 13
- Lecture 4: Invariant Verification, Sept 18
- Homework 1, Due Oct 2
- Lecture 5: Invariant Verification, Sept 20
- Lecture 6: Symbolic Reachability Analysis, Sept 25
- Lecture 7: BDDs, Symmetry, Sept 27
- Lecture 8: Symmetry, Safety reuiqrements Oct 2
- Lecture 9: STL Model checking, Oct 4
- Lecture 10: Expressiveness, Oct 9
- Lecture 11: Automata, Refinement Oct 11
- Homework 2, Due Nov 2
- Lecture 12: Assume guarantee reasoning Oct 16
- Lecture 13: Simulation and refinement Oct 18
- Lecture 14: Omega languages, Nov 1
- Lecture 15: Fair modules, Nov 6
- Lecture 16: Runtime Verification by Oleg Sokolsky, Nov 8
- Lecture 17: Response verification, Nov 13
- Lecture 18: Temporal liveness requirements, Nov 15
- Lecture 19: Symbolic model checking, automata, Nov 20
- Lecture 20: Linear Temporal Logic, Nov 20
- Lecture 21,22: Software Model checking with SLAM, Nov
27,29
- Lecture 23: Games, Dec 4
- Lecture 24: Nested words and trees Dec 6
Last updated on September 6, 2006 by Rajeev Alur