Efficiency analysis of formally verified adaptive cruise controllers

We consider an adaptive cruise control system in which control decisions are made based on position and velocity information received from other vehicles via V2V wireless communication. If the vehicles follow each other at a close distance, they have better wireless reception but collisions may occur when a follower car does not receive notice about the decelerations of the leader car fast enough to react before it is too late. If the vehicles are farther apart, they would have a bigger safety margin, but the wireless communication drops out more often, so that the follower car no longer receives what the leader car is doing. In order to guarantee safety, such a system must return control to the driver if it does not receive an update from a nearby vehicle within some timeout period. The value of this timeout parameter encodes a tradeoff between the likelihood that an update is received and the maximum safe acceleration. Combining formal verification techniques for hybrid systems with a wireless communication model, we analyze how the expected efficiency of a provably-safe adaptive cruise control syst em is affected by the value of this timeout.

@inproceedings{DBLP:conf/itsc/LoosWSP13,
	pdf = {pub/dccs-efficiency.pdf},
	slides = {pub/dccs-efficiency-slides.pdf},
	study = {pub/dccs-efficiency-examples.zip},
	author = {['Sarah M. Loos', 'David Witmer', 'Peter Steenkiste', 'André Platzer']},
	title = {Efficiency Analysis of Formally
               Verified Adaptive Cruise Controllers},
	booktitle = {ITSC},
	longbooktitle = {Intelligent Transportation Systems
              (ITSC), 16th International IEEE
              Conference on, October 6-9, The
              Hague, Netherlands, Proceedings},
	year = {2013},
	pages = {1565-1570},
	doi = {10.1109/ITSC.2013.6728453},
	editor = {['Andreas Hegyi', 'Bart De Schutter']},
	isbn = {978-1-4799-2914-613},
	keywords = {Traffic theory for ITS, Network
               modeling, Driver assistance systems,
               V2V wireless communication,
               Hybrid systems, Formal verification},
	abstract = {

  We consider an adaptive cruise control system
in which control decisions are made based on position
and velocity information received from other vehicles
via V2V wireless communication. If the vehicles
follow each other at a close distance, they have
better wireless reception but collisions may occur
when a follower car does not receive notice about the
decelerations of the leader car fast enough to react
before it is too late. If the vehicles are farther
apart, they would have a bigger safety margin, but
the wireless communication drops out more often, so
that the follower car no longer receives what the
leader car is doing. In order to guarantee safety,
such a system must return control to the driver if it
does not receive an update from a nearby vehicle
within some timeout period. The value of this timeout
parameter encodes a tradeoff between the likelihood
that an update is received and the maximum safe
acceleration. Combining formal verification
techniques for hybrid systems with a wireless
communication model, we analyze how the expected
efficiency of a provably-safe adaptive cruise control
syst em is affected by the value of this timeout.
  }
}