CIS 573: Computer-Aided Verification, Fall 1997
Class: Mon Wed 3-4.30, Towne 303
Office hours: Tues 1-3, Moore 276, and by appointment
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 digital 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.
The course requires basic knowledge of algorithms, data structures,
automata theory, and
propositional(boolean) logic (CSE 262, or equivalent).
Knowledge of operating systems, communication protocols,
and hardware (CSE 380) is useful.
Besides graduate and advanced undergraduate CSE students,
EE students interested in design automation,
and Math students interested in applications of logic to computer
science are welcome.
If you need more information to decide, contact the instructor.
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, realizability and control, minimization.
- Verification techniques:
symbolic model checking, on-the-fly model
checking, state space reduction methods, compositional and
hierarchical reasoning, abstract interpretation.
We will use the following two software tools (installed on gradient)
A variety of
Click
other tools support computer-aided verification.
The course will use the draft of a forthcoming textbook
titled Computer-aided verification by Alur & Henzinger.
The article
"Computer-aided verification", E.M. Clarke and R.P. Kurshan,
IEEE Spectrum, 1996,
provides an overview of the state of the art.
Following books are on reserve in Engineering Library for
additional reading
-
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
There will be periodic homework assignments consisting of
theoretical problems and experimentation with SPIN and SMV.
There will be no exams.
The major component of the evaluation will be the class project.
The project can be done in groups of two or three, and will
require a presentation in the final week.
Projects can be of various forms:
- Programming: Implementation of algorithms in the programming
environment MOCHA
- Case study: Modeling, specification, and analysis
of an application design
- Tool Comparison: Using different model checkers to model
and analyze the same design to understand differences between
various approaches
- Surveys: Read a few papers on a realted topic not covered
in the class
- Theory: Exploratory research
- 9/3:Introduction
Viewgraphs
- 9/8: Modeling language: reactive modules
Viewgraphs
- 9/10: No class scheduled
- 9/15: Reactive modules continued
Viewgraphs
- 9/17: Invariant verification
Viewgraphs
- Homework 1: Due 9/29
- 9/22: Invariant verification continued
Viewgraphs
- 9/24: Selective search using partial-order reduction
Viewgraphs
- 9/29: Partial-order reduction continued and introduction to SPIN
Viewgraphs
- 10/1: Symbolic search and BDDs
Viewgraphs
- Homework 2: Due 10/23
- 10/6: Symbolic search using BDDs contd.
Viewgraphs
- 10/8: Stable partitions and Symmetries
Viewgraphs
- Week of 10/6: Project assignments
- 10/13: Fall break, no class
- 10/15: Partition Refinement Algorithms
Viewgraphs
- 10/20: NO CLASS
- Homework 3: Due 11/5
- 10/22: Safe temporal logic
Viewgraphs
- 10/27: STL model checking, distinguishing and expressive power
Viewgraphs
- 10/29: Automata-theoretic safety verification
Viewgraphs
- 11/3: Trace semantics, compositionality, asssume-guarantee
Viewgraphs
- 11/5: Simulation relations, homomorphisms
Viewgraphs
- 11/10: Omega-languages, safety versus liveness
Viewgraphs
- 11/12: Fair modules
Viewgraphs
- Homework 4: Due 12/8
- 11/17: Searching for fair cycles and response verification
Viewgraphs
- 11/19: Searching for Buchi cycles; Computation tree logic CTL
Viewgraphs
- 11/24: Mu-calculus / Bow-Yaw: Security protocols
Viewgraphs
- 11/26: Symbolic model checking / Yerang: Cache coherence protocols
Viewgraphs
- 12/1: Theory of omega-regular languages/ Moonjoo: Minimization of timed systems
Viewgraphs
- 12/3: Linear temporal logic LTL; Olaf/Yael: BMDs and HDDs;
Mahesh: Membership problems for timed/hybrid automata
Viewgraphs
- 12/8: NO CLASS
- 12/10: Wrap-up; Xiahuo: Testing;
Karthik/Davor: case-study of village telephone system
Last updated on October 27, 1997.