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. .pdf Also, Technical Report MIT/LCS/TR-730, Laboratory for Computer Science, Massachusetts Institute of Technology, September 1997.

For a comference version refer to:

Carolos Livadas and Nancy A. Lynch. Formal Verification of Safety-Critical Hybrid Systems. Proceedings of 1st International Workshop, Hybrid Systems: Computation and Control (HSCC'98, Berkeley, CA, April 1998), volume 1386 of Lecture Notes in Computer Science. Springer-Verlag 1998. Abstract/Paper

Abstract

This thesis investigates how the formal modeling and verification techniques of computer science can be used for the analysis of hybrid systems [1,2,3,4]---systems involving both discrete and continuous behavior. The motivation behind such research lies in the inherent similarity of the hierarchical and decentralized control strategies of hybrid systems and the communication and operation protocols used for distributed systems in computer science. As a case study, the thesis focuses on the development of techniques that use hybrid I/O automata [5,6] to model and analyze automated vehicle transportation systems and, in particular, their various protection subsystems---control systems that are used to ensure that the physical plant at hand does not violate its various safety requirements.

The thesis is split into two major parts. In the first part, we develop an abstract model of a physical plant and its various protection subsystems---also referred to as protectors. The specialization of this abstract model results in the specification of a particular automated transportation system. Moreover, the proof of correctness of the abstract model leads to simple correctness proofs of the protector implementations for particular specializations of the abstract model. In this framework, the composition of independent protectors is straightforward---their composition guarantees the conjunction of the safety properties guaranteed by the individual protectors. In fact, it is shown that under certain conditions composition holds for dependent protectors also.

In the second part, we specialize the aforementioned abstract model to simplified versions of the personal rapid transit system (PRT 2000^TM) under development at Raytheon Corporation. We examine overspeed and collision protection for a set of vehicles traveling on straight tracks, on binary merges, and on a directed graph of tracks involving binary merges and diverges. In each case, the protectors sample the state of the physical plant and take protective actions to guarantee that the physical plant does not reach hazardous states. The proofs of correctness of such protectors involve specializing the abstract protector to the physical plant at hand and proving that the suggested protector implementations are correct. This is done by defining simulations among the states of the protector implementations and their abstract counterparts.

References

1 Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors. Hybrid Systems, volume 736 of Lecture Notes in Computer Science. Springer-Verlag, 1993. This volume of LNCS was inspired by a workshop on the Theory of Hybrid Systems, held on Oct. 19-21, 1992 at the Technical University, Lyngby, Denmark, and by a prior Hybrid Systems Workshop, held on June 10-12, 1991 at the Mathematical Scsiences Institute, Cornell University.

2 Amir Pnueli and Joseph Sifakis, editors. Special Issue on Hybrid Systems, volume 138, part 1 of Theoretical Computer Science. Elsevier Science Publishers, February 1995.

3 Michael S. Branicky. Studies in Hybrid Systems: Modeling, Analysis, and Control. Doctor of Science Thesis, Dept. of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts, June 1995.

4 John Lygeros. Hierarchical, Hybrid Control of Large Scale Systems. Doctor of Philosophy Thesis, Dept. of Electrical Engineering and Computer Sciences, University of California, Berkeley, May 1996.

5 Nancy Lynch, Roberto Segala, Frits Vaandrager, and H. B. Weinberg. Hybrid I/O Automata. In R. Alur, T. Henzinger, and E. Sontag, editors, Proc. DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems, Hybrid Systems III: Verification and Control, volume 1066 of Lecture Notes in Computer Science, pages 496-510. Springer-Verlag, 1996. The DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems took place in New Brunswick, New Jersey, in October 1995.

6 Nancy Lynch, Roberto Segala, Frits Vaandrager, and H. B. Weinberg. Hybrid I/O Automata. Preprint, August 1997.

Table of Contents

Preface

1. Introduction

2. Hybrid I/O Automata

3. Abstract Physical Plant and Protector Models

4. Modeling a System of n Vehicles

5. Example 1: Overspeed Protection System

6. Example 2: Collision Avoidance on a Single Track

7. Example 3: Collision Avoidance on Merging Tracks

8. Example 4: Collision Avoidance on a General Graph of Tracks

9. Composing the Overspeed and Collision Avoidance Protection Systems

10. Conclusions and Future Work

References