Skip to main content
SpringerLink
Log in

Verification of automated vehicle protection systems

Extended abstract

  • Conference paper
  • First Online:
Hybrid Systems III (HS 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1066))

Included in the following conference series:

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 selected safety properties for automated Personal Rapid Transit (PRT) systems such as PRT 2000™, a system currently being developed at Raytheon. 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 that enforce speed limits and vehicle separation.

Research supported an NSF Graduate Fellowship and the grants and contracts below.

Research supported by NSF Grant 9225124-CCR, U.S. Department of Transportation Contract DTRS95G-0001-YR.8, AFOSR-ONR Contract F49620-94-1-0199, and ARPA Contracts N00014-92-J-4033 and F19628-95-C-0118.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Nancy Lynch and Frits Vaandrager. Forward and backward simulations — Part II: Timing-based systems. Technical Memo MIT/LCS/TM-487.C, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA 02139, April 1995. To appear in Information and Computation.

    Google Scholar 

  2. Nancy Lynch. Modelling and verification of automated transit systems, using timed automata, invariants and simulations. This volume.

    Google Scholar 

  3. Nancy Lynch, Roberto Segala, Frits Vaandrager, and H.B. Weinberg. Hybrid I/O automata. This volume.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MIT Laboratory for Computer Science, 02139, Cambridge, MA

    H. B. Weinberg

  2. Raytheon Company, 1001 Boston Post Road, 01752, Marlborough, MA

    Norman Delisle

Authors
  1. H. B. Weinberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nancy Lynch
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Norman Delisle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Rajeev Alur Thomas A. Henzinger Eduardo D. Sontag

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Weinberg, H.B., Lynch, N., Delisle, N. (1996). Verification of automated vehicle protection systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds) Hybrid Systems III. HS 1995. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020938

Download citation

  • DOI: https://doi.org/10.1007/BFb0020938

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61155-4

  • Online ISBN: 978-3-540-68334-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation