Models and Analysis of Real-Time and Hybrid Systems

G22.3033-007
Tuesday, 5:00-7:00 PM
Room 813 WWH
Amir Pnueli

Reaching Me

Amir Pnueli

Prerequisites: Some background in algorithm design, familiarity with the language of first-order logic, and at least one imperative and one functional programming language.

Course requirements: Assignments and a term project.

Course Description

Hybrid systems are systems which combine discrete and continuous components. Most systems in which a hardware plant controlled by a program (e.g an airplane controlled by a fly-by-wire software, or a computerized robot navigating in a physical environment) are hybrid in nature. The reliable construction of such systems requires modeling and analysis techniques which combine discrete and continuous methods. In this course we introduce the basic models and analysis techniques that can aid in the design and construction of hybrid systems.

The class of computer systems whose modeling, analysis, and development are most challenging is the class of reactive systems. 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 research field.

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

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.

Course topics:

Class Presentations

Assignments

TLV Resources

Files and Programs