Timed and Hybrid Systems
Monday, 5:00-6:50 PM
Room 513, WWH
Prerequisites: Some background in
algorithm design, familiarity with the language of first-order logic,
and parallel programs.
- phone: (212) 998-3225
- office: WWH, Room 505
- office hours: Monday, Wednesday 3:30-5:00 PM, or by appointment
Assignments and a
Recommended: Temporal Verification of Reactive Systems: Safety
by Zohar Manna and Amir Pnueli, Springer-Verlag
The class of computer systems whose modeling, analysis, and
development are most challenging is the class of
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
Network protocols, Air traffic control system, Programs controlling
mechanical devices such as a train, a plane, or ongoing processes such
as a nuclear reactor. Recently, there is an awakened interest in
reactive systems due to the emergence of embedded systems as a major
The Formal Methods approach to software analysis and 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 level of abstraction can be used in the study of reactive and
embedded systems. At the highest level of abstraction, we only care
about the temporal precedence of events and actions, and can guarantee
that a system satisfies a requirement such as "every request is
eventually followed by a response". However, at this level of modeling
we cannot bound the response time by actual numbers. In the course, we
consider two successive refinements of our modeling and specification
abilities. The first refinement considers the model of
real-time systems. In this model, we
represent, specify, and analyze the temporal distance between events,
thus being able to require and verify a property such as "every request is
eventually followed by a response, which must occur within the time
interval [3,5] from the request".
The next level of refinement considers the model of
hybrid systems. In this model, we
consider a system consisting of a combination of components some of
which are discrete, such as programs, while the other are continuous,
such as a motor driving a railroad gate barrier. This model employs
discrete as well as continuous analysis tools in order to analyze and
verify the correctness of hybrid systems, typically corresponding to a
digital program controlling a continuous environment.
- The computational model of Real-Time Systems (RTS).
- A simple programming language (SPL),extended by timing
information and its translation into RTS.
- The specification language of Timed Temporal Logic (TTL).
- Discrete and dense-time Timed Automata.
- Model checking timed properties of timed automata.
- Deductive verification of timed properties.
- The computational model of Hybrid Systems.
- Hybrid automata.
- Model checking properties of hybrid automata.
- Verification Diagrams.
- Deductive verification of Hybrid Systems.
Lecture 1 -- January 22, 2007:
Lecture 2 -- January 29, 2007:
Lectures 3,4 -- February 5, 2007:
Lectures 5 -- February 12, 2007:
Lectures 6 -- February 26, 2007:
Lectures 7 -- March 5, 2007:
Lectures 8 -- March 26, 2007:
Lectures 9 -- April 2, 2007:
Lectures 10 -- April 10, 2007:
Lectures 11 -- April 16, 2007:
Lectures 12 -- April 23, 2007: