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.
[postscript, pdf, bib]

For a complete version refer to: 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/Thesis

Also, Technical Report MIT/LCS/TR-730, Laboratory for Computer Science, Massachusetts Institute of Technology, September 1997.

Abstract

This paper investigates how formal techniques can be used for the analysis and verification of hybrid systems [GNRR93,PS95,Branicky-ScD,Lygeros-PhD]---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. This paper focuses on the use of hybrid I/O automata [LSVW95,LSVW97] to model, analyze, and verify safety-critical hybrid systems that use emergency control subsystems to prevent the violation of their safety requirements. The paper is split into two parts. First, we develop an abstract model of a protector---an emergency control component that guarantees that the physical plant at hand adheres to a particular safety requirement. The abstract protector model specialized to a particular physical plant and a particular safety requirement constitutes the specification of a protector that enforces the particular safety property for the particular physical plant. The correctness proof of the abstract protector model leads to simple correctness proofs of the implementations of particular protectors. In addition, the composition of independent protectors, and even dependent protectors under mild conditions, guarantees the conjunction of the safety properties guaranteed by the individual protectors being composed. Second, as a case study, we specialize the aforementioned abstract protector model to simplified versions of the personal rapid transit system (\PRT) under development at Raytheon Corporation and verify the correctness of overspeed and collision avoidance protectors. Such correctness proofs are repeated for track topologies ranging from a single track to a directed graph of tracks involving Y-shaped merges and diverges.

References

[GNRR93] 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 Sciences Institute, Cornell University.

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

[Branicky-ScD] 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.

[Lygeros-PhD] 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.

[LSVW95] 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.

[LSVW97] Nancy Lynch, Roberto Segala, Frits Vaandrager, and H. B. Weinberg. Hybrid I/O Automata. Preprint/Work in Progress, June 1997.