Nancy Lynch. Modelling 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-545, Laboratory for Computer Science, Massachusetts Institute of Technology. .pdf

Abstract

This paper contains an overview of work in the TDS group on modelling, verifying and analyzing problems arising in automated transit systems. These problems are inspired by work at Raytheon and in the California PATH project. It is based on the hybrid I/O automaton model . The formal techniques we use include standard techniques for reasoning about concurrent algorithms -- invariants, simulations (levels of abstraction) and automaton composition, plus standard moehods for reasoning about continuous processes -- differential equations.