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: