CSE 625: Computer Aided Verification, Spring 2003

(Listed as Asynchronous Systems)

[Announcements][Homeworks][Project]

Instructor: Radu Grosu ( grosu@cs.sunysb.edu),

Class: TueThu 2:20pm - 3:40pm, Melville Library room N4006

Office hours: TueThu 4-5pm, CS Building room 1425, and by appointment

Motivation

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 complex 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.

Objectives

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.

Prerequisites

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.

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 of reactive systems: states and events, nondeterminism and concurrency, synchrony and asynchrony, real-time and hybrid systems, open systems.
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.

Software

We will use the model checker MOCHA being currently developed at Stony Brook, UPenn and UC Berkeley.

Related tools include

Reading

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
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 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 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 related topic not covered in the class
Theory: Exploratory research