Analysis of Reactive Systems, Algorithmic and Deductive Methods
Thursday, 5:00-6:50 PM
Room 317, CIWW
- phone: (212) 998-3225
- office: CIWW, Room 402
- office hours: Wednesday 2:00-4:00 PM, or by appointment
All students should register themselves with the class list, which is used for
all technical discussions concerning the course and the course project.
To subscribe to this list visit the web page:
where you will find full directions.
Please send all your questions to this list (not only to the instructor) so
that everyone can participate.
Prerequisites: Some background in
algorithm design, familiarity with the language of first-order logic,
and parallel programs.
Assignments and a term project.
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.
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
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 CVC, PVS or STeP for verifying the properties of programs.
Towards the end of the semester, we will consider the use of the
notions of reactive systems, their specification, and verification for
the modeling of Biological systems at a certain level of abstraction.
- The computational model of Fair Discrete Systems (FDS).
- A simple programming language (SPL) and its translation into FDS.
- The specification language of linear temporal logic (LTL).
- Finite-State Systems and their Verification (Model Checking).
- A programmable model checker TLV.
- The PVS Theorem prover. Encoding FDS's and LTL within PVS.
- Verifying invariance properties.
- Algorithmic construction of auxiliary invariants.
- Verifying progress properties.
- The CHAIN and WELL rules.
- Verification Diagrams.
- Verifying progress under compassion.
- Verifying general LTL properties.
- Modeling Biological Systems as Reactive Systems.
Lecture 1 -- September 10, 2009:
slides (lecture1.ps) ,
Lecture 2 -- September 17, 2009:
Lecture 3 -- September 24, 2009:
Lecture 4 -- October 1, 2009:
Lecture 5 -- October 15, 2009:
Lecture 6 -- October 22, 2009:
Lecture 7 -- November 5, 2009:
Lecture 8 -- November 12, 2009:
Lecture 9 -- November 19, 2009:
Lecture 10 -- December 3, 2009:
Lecture 11 -- December 10, 2009:
Lecture 12 -- December 15, 2009: