H. B. Weinberg and Nancy Lynch. Correctness of Vehicle Control Systems -- A Case Study. 17th IEEE Real-Time Systems Symposium, Washington, D. C., pages 62-72, December 1996. .pdf For a full version of this paper see H. B. Weinberg's thesis.

Abstract

The hybrid I/O automaton (HIOA) model of Lynch, Segala, Vaandrager and Weinberg is used to specify and verify part of an automated transportation system -- a vehicle deceleration maneuver. Four deceleration controllers are considered: with and without communication delay, and with and without feedback. Safety and timeliness properties are proved.

The methods used include automaton composition, invariant assertions and simulation mappings, as well as simple differential equations. The proofs are clear and scale well from the simplest case to the feedback with delay case. This case study demonstrates the applicability of the model and methods to automated transportation systems in particular, and to hybrid systems in general.