Analysis of Reactive Systems

G22.3033-005
Monday, 5:00-6:50 PM
Room 102, WWH
Amir Pnueli

Reaching Me

Amir Pnueli

Prerequisites: Some background in algorithm design, familiarity with the language of first-order logic, and parallel programs.

Course requirements: Assignments and a term project.

Textbooks:
Recommended: "Temporal Verification of Reactive Systems: Safety" by Zohar Manna and Amir Pnueli, Springer-Verlag.

"Model Checking", by E.C. Clarke and O. Grumberg and D. Peled, MIT Press, 2000.

Course Description

Reactive systems are systems whose role is to maintain an ongoing interaction with their environment rather than produce some final value upon termination. Typical examples of reactive systems are Air traffic control system, Programs controlling mechanical devices such as a train, a plane, or ongoing processes such as a nuclear reactor.

The Formal Methods approach to software construction is based on viewing a program and its execution as mathematical objects and applying mathematical and logical techniques to specify and analyze the properties and behavior of these objects. The main advantages of the formal approach to software construction is that, whenever applicable, it can lead to an increase of the reliability and correctness of the resulting programs by several orders of magnitude.

Several approaches to the verification of reactive systems are available, the most prominent of which are Algorithmic (model checking) and Deductive verification. In this semester we will consider both of these approaches. Under algorithmic verification we will show how to verify properties of finite-state systems. Under deductive verification, we use theorem-proving techniques to establish the correctness of infinite-state reactive programs relative to their temporal specifications. We will be using computer-aided theorem provers such as PVS and STeP for verifying the properties of programs.

Course topics:

Class Presentations

Resources

Assignments

Term Project