CSE 625: Computer Aided Verification, Spring 2003
(Listed as Asynchronous Systems)
- 3:40pm, Melville Library room N4006
Office hours: TueThu 4-5pm, CS Building room
1425, and by appointment
Reactive systems are becoming an integral part of nearly every engineered
product: they control consumer products, commercial aircraft, nuclear power
plants, medical devices, weapon systems, aerospace systems, automobiles,
public transportation systems, and so on. At the same time quality
and confidence issues are increasing in importance. Errors may result in
loss of life, destruction of property, failure of businesses, and environmental
harm. Today, designers check that a reactive system works properly
by using simulation and testing. However, as reactive systems become more
and pervasive, these traditional techniques are not sufficient to assure
desired reliability. Model checking and related computer-aided verification
techniques are emerging as practical alternatives. They allow the designer
to verify that a mathematical model of a system satisfies its abstract
logical specification. This approach has been most effective for control-intensive
components, and is rapidly becoming an integral part of the design cycle
in many companies.
The participants will learn how to model a reactive
(hardware or software) sytem, express desired properties of the reactive
system and check that the system satisfies these properties. They will
get familiar with the algorithmic methods used for this check.
The course requires basic knowledge of algorithms, data structures, automata
theory, computational complexity, and propositional logic. 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.
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.
Models of reactive systems: states and events, nondeterminism and
concurrency, synchrony and asynchrony, real-time and hybrid systems, open
Properties of reactive sytems: safety and liveness, linear and branching
temporal logic, refinement preorders.
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 model checker MOCHA
being currently developed at Stony Brook, UPenn and UC Berkeley.
Related tools include
The course will use the draft of a forthcoming textbook titled Computer-aided
verification by R. Alur & T. Henzinger. Chapters will be posted
on the web as needed.
Following books are recommended for additional reading
Model Checking, E.M. Clarke, O. Grumberg and D.A. Peled. MIT Press. 2000
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
There will be periodic homework assignments consisting of problems and
experimentation with MOCHA.
There will be no exams.
There will be a 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
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 related topic not covered in the class
Theory: Exploratory research
Modeling Lanuage Reactive Modules
1/28, 1/30: Definition, operations on reactive modules, examples
2/4,6: Transition graphs, invariants, graph traversal, state explosion,
Symbolic Graph Search
2/11,13: Symbolic invariant verification, binary decision diagrams
2/18,20: Graph partitions, partition refinement, reachable partition refinement
Temporal Safety Requirements
2/25: State logics, safe temporal logic STL
2/27: STL model checking, distinguishing and expressive power
Automata-theoretic Safety Verification
3/4: Automata, safe automata logic SAL, operations on automata, model checking7:
3/6: Trace semantics, compositionality, asssume-guarantee
3/11: Simulation relations, homomorphisms
3/13: Omega-languages, safety versus liveness
3/25: Fairness, fair modules, examples
3/27: Searching for fair cycles and response verification
Temporal Liveness Requirements
4/1: CTL, Mu-calculus, and Symbolic model checking
Automata-theoretic Liveness Verification
4/3: Theory of omega-regular languages
Linear Temporal Logic
4/8: Linear temporal logic LTL
4/10,15: MSCs, hierarchical modules, and UML
Week of 5/1: Project presentations
Last updated on Feb 4, 2003 by Radu