Formal Modeling, Analysis, and Verification of Hybrid Systems

Background

The recent trend towards system integration and computer automation has lead to the emergence of very complex hybrid systems --- dynamical systems that involve both discrete and continuous behavior and/or components. To date, the validation of hybrid systems has predominantly been accomplished by simulation testing. However, as systems get more complex, the exhaustive testing of all possible system behaviors becomes unrealistic and, subsequently, the confidence in such validation schemes is diminished.

The safety-critical nature of numerous hybrid systems, such as automated transportation systems, has encouraged the formal modeling and validation through deductive reasoning. This approach not only forces the system designers to produce formal specifications of the system's behavior, but provides irrefutable proof that a system satisfies its safety requirements. When generating the formal specifications of a system's behavior, it is helpful to take advantage of modular decomposition and abstraction. The generation of specifications in a modular fashion emphasizes the component structure of the system and simplifies the modeling process by focusing attention to a single component at a time. The use of abstraction allows the system designers to ignore inessential system behavior, to use nondeterminism in a system's description, and to allow reasoning about the system behavior at a high level.

Why is this research interesting?

The advantages of a formal approach to modeling, analyzing, and validating hybrid systems --- in particular, safety-critical automated transportation systems --- are numerous. First, this approach produces a clear and precise model of the system that is both abstract (that is, inessential system details are omitted) and complete (all components of the system, including environment models, are modeled). Second, the deductive reasoning techniques and well-established proof techniques from CS and control theory may be used to validate system properties. It is important to note that this validation process is formal, in the sense that, under prespecified assumptions, any behavior of the system satisfies the properties that are verified.

Approach

In order to model hybrid systems, the TDS group has been developing a mathematical framework denoted the hybrid I/O automaton (HIOA) model. In this model, a hybrid system is specified as a set of automata that share variables and discrete transitions. The discrete behavior of a system is described by a set of discrete state transitions; discrete transitions shared among automata synchronize based on transition labels. The continuous behavior of a system is described by a set of trajectories which specify the behavior of the variables of an automaton with time.

The HIOA formal model has evolved to its latest form through the modeling of various automated transportation systems. The modeling efforts of the TDS group have been guided by the actual designers of the various systems, who have often assisted so as to guarantee that the system models are truthful descriptions of the behavior of the actual systems.

The proof methods that are used are assertional. They involve either proofs that the system satisfies a particular invariant, or proofs that a refined model of the system actually implements a more abstract model (simulation relations). It is important to note that assertions can involve timing information; that is, predicates on continuous variables of the system. Since the behavior of HIOA involves both discrete transitions and trajectories, proof techniques from control theory must be used to reason about the continuous system behavior. However, through multiple discrete and hybrid system case studies, the TDS group has become proficient in determining when and how to use proof techniques from CS and control theory. The key is to reason about discrete and continuous system behavior independently and, subsequently, to combine the individual results so as to prove a particular property of the hybrid behavior.

Furthermore, it is important to note that due to modular system decomposition and abstraction, the HIOA modeling and validation proofs can scale to larger and more complex hybrid systems. This is achieved by reasoning about the system's behavior at a high level of abstraction and showing that more refined system models are actual implementations of their abstract counterparts.

Progress

To date, the TDS group has successfully modeled and verified several hybrid systems in the area of automated transit. One such system is the automated highway system of the California PATH project. Recently, Dolginova and Lynch have used HIOA to model and verify the safety of the platoon join maneuver --- a maneuver in which two adjacent vehicle platoons join to form a single platoon. In the realm of personal rapid transit, the TDS group has modeled the PRT 2000TM system under development at Raytheon Corporation. For various track topologies, it was verified that the vehicles comprising the system neither exceed a prespecified speed limit, nor collide among themselves. While modeling this system, Livadas and Lynch developed an abstract model of a protector --- a protection subsystem that guarantees a particular safety property under a set of assumptions. The advantage of this model is that the proof of correctness of particular protector implementations get reduced to simple simulation proofs from the implementation to the abstract model.

Recently, Lygeros, Livadas, and Lynch have been modeling and analyzing the traffic alert and collision avoidance system (TCAS II version 7) that is being used by aircraft to avoid midair collisions. The modeling approach involves specifying all components of the system which in this case not only involves the system hardware but also the aircraft pilots. Currently, Lygeros et al. are in the process of proving correctness of the TCAS algorithm for an ideal system (a system with no delays, no uncertainties, and exact sensors). The goal is to be able to prove that under particular assumptions the TCAS system will prevent aircraft collisions. Since the validation techniques to be used scale to more complex systems, once the correctness of TCAS is shown for the ideal system, the reintroduction of delays and uncertainties should be straightforward.

The following is a list of the various hybrid systems that have been analyzed by the TDS group using formal methods:

In all of the above applications, the analyses emphasize safety properties. However, performance properties such as maximum speed and throughput, timely arrival, and passenger comfort may also be addressed in the future. An interesting modeling twist will involve the explicit modeling of uncertainty in the various systems, such as time lag of information provided by sensors, unknown delays in communication, uncertainty in vehicle response (e.g., wheel slippage or inexact propulsion system performance), and inexact processor clocks. Moreover, an extension of such research may involve fault tolerance analyses of the various hybrid system designs, such as communication and processor failures and vehicle and roadway malfunctions.

The survey paper "Modeling and verification of automated transit systems, using timed automata, invariants and simulations," authored by Prof. Lynch, summarizes the research on hybrid systems conducted by the Theory of Distributed Systems group up to Dec. 1995.

Related Publications

Ekaterina Dolginova and Nancy Lynch. Safety Verification for Automated Platoon Maneuvers: A Case Study. In International Workshop on Hybrid and Real-Time Systems (HART'97, Grenoble, France, March 26-28, 1997), volume 1201 of Lecture Notes in Computer Science, pages 154-170. Springer-Verlag 1997. (Abstract/Postscript)

Connie Heitmeyer and Nancy Lynch. The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time System. Proceedings of the 15th IEEE Real-Time Systems Symposium, pages 120--131, San Juan, Puerto Rico, December 1994. IEEE Computer Society Press. (Abstract/Postscript) Also, Technical Memo MIT/LCS/TM-511, Laboratory for Computer Science, Massachusetts Institute of Technology, November 1994. (Abstract/Postscript)

Gunter Leeb and Nancy Lynch Proving Safety Properties of the Steam Boiler Controller. In Jean-Raymond Abrial, Egon Boerger, and Hans Langmaack, editors, Proceedings of Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, volume 11654 of Lecture Notes in Computer Science, Springer-Verlag 1996. (Abstract/Postscript)

Carolos Livadas, Formal Verification of Safety-Critical Hybrid Systems, Master of Engineering Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, September 1997. (Abstract/Postscript) Also, Technical Report MIT/LCS/TR-730, Laboratory for Computer Science, Massachusetts Institute of Technology, September 1997.

John Lygeros and Nancy Lynch. On the Formal Verification of the TCAS Conflict Resolution Algorithms. Proceedings of the 36th IEEE Conference on Decision and Control, San Diego, CA, December 1997. (Summary/Postscript)

Nancy Lynch. A Three-Level Analysis of a Simple Acceleration Maneuver, with Uncertainties. Proceedings of the Third AMAST Workshop on Real-Time Systems, pages 1-22, Salt Lake City, Utah, March 1996. Also, AMAST Workshops on Real-Time Systems 95 & 96, AMAST Series in Computing, World Scientific Publishing Company. (Abstract/Postscript)

Nancy Lynch. Modeling and verification of automated transit systems, using timed automata, invariants and simulations. In R. Alur, T. Henzinger, and E. Sontag, editors, Hybrid Systems III: Verification and Control (DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, October 1995), volume 1066 of Lecture Notes in Computer Science, pages 449-463. Springer-Verlag 1996. Also, Technical Memo MIT/LCS/TM-544, Laboratory for Computer Science, Massachusetts Institute of Technology. (Abstract/Postscript).

Nancy Lynch and H.B. Weinberg. Proving Correctness of a Vehicle Maneuver: Deceleration In the Second European Workshop on Real-Time and Hybrid Systems, Grenoble, France, June 1995.(Compressed Postscript)

TOC / LCS / MIT
Last modified: 2002/11/19, 20:26:29. 		Comments?