H. B. Weinberg, Nancy Lynch, and Norman Delisle. Verification of Automated Vehicle Protection Systems. 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 101-113. Springer-Verlag 1996. .pdf

Abstract

We apply specification and verification techniques based on the timed I/O automaton model of Lynch and Vaandrager to a case study in the area of automated transit. The case study models and verifies some of the safety properties of a Personal Rapid Transit (PRT) system currently being developed at Raytheon, called PRT-2000. Due to their safety critical nature, PRT-2000 and many other automated transit systems divide the control architecture into operation and protection subsystems. The operation system handles the normal control of vehicles. The protection system maintains safety by monitoring and possibly taking infrequent but decisive action. In this work, we present both a high-level treatment of a generic protection system and more detailed examinations of protection systems which enforce speed limits and vehicle separation.