Stefan Mitsch, Sarah M. Loos, Andre Platzer,
"Towards formal verification of freeway traffic control"
, in Chenyang Lu: Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems (ICCPS '12), IEEE Computer Society, Washington, DC, USA, Seite(n) 171-180, 2012, ISBN: 978-0-7695-4695-7
Towards formal verification of freeway traffic control
Sprache des Titels:
Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems (ICCPS '12)
We study how CPS technology can help improve freeway traffic by combining local car GPS positioning, traffic center control decisions, and communication to achieve more tightly coupled feedback control in intelligent speed adaptation. We develop models for an intelligent speed adaptation that respects variable speed limit control and incident management. We identify safe ranges for crucial design parameters in these systems and, using the theorem prover KeYmaera, formally verify safety of the resulting CPS models. Finally, we show how those parameter ranges can be used to decide trade-offs for practical system implementations even for design parameters that are not modeled formally.