Safety Verification of Automated Vehicle Maneuvers

Work Done by Ekaterina Dolginova and Nancy Lynch

Dolginova and Lynch formally model a system consisting of two vehicles moving along a single track, plus controllers that operate the vehicles, plus communication channels. The modeling formalism used is the Hybrid Automata model developed by Lynch, Segala, Vaandrager and Weinberg. We formulate a key safety requirement of such a system, namely, that the two vehicles never collide at a relative velocity greater than a given bound. We give necessary and sufficient conditions for the controller of the follower vehicle to guarantee that the safety requirement is satisfied regardless of the behavior of the leading vehicle. The model includes handling of communication delays and inexactness of sensors and brakes. The proofs use composition, invariants, and levels of abstraction, together with methods of mathematical analysis. This case study is derived from the California PATH intelligent highway project.

Additionally, Mike Branicky in collaboration with Dolginova and Lynch has developed a toolbox that can be used in proving some invariant properties of hybrid systems.

Papers Written: