DocumentCode :
2041760
Title :
Towards Formal Verification of Freeway Traffic Control
Author :
Mitsch, Stefan ; Loos, Sarah M. ; Platzer, André
Author_Institution :
Johannes Kepler Univ., Linz, Austria
fYear :
2012
fDate :
17-19 April 2012
Firstpage :
171
Lastpage :
180
Abstract :
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.
Keywords :
Global Positioning System; control engineering computing; feedback; formal verification; road traffic control; theorem proving; traffic engineering computing; velocity control; CPS technology; KeYmaera theorem prover; coupled feedback control; cyber-physical system; formal verification; freeway traffic control; freeway traffic improvement; incident management; intelligent speed adaptation; local car GPS positioning; traffic center control communication; traffic center control decisions; variable speed limit control; Acceleration; Adaptation models; Artificial intelligence; Detectors; Safety; Traffic control; Vehicles; Freeway traffic control; hybrid system; intelligent speed adaptation;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Cyber-Physical Systems (ICCPS), 2012 IEEE/ACM Third International Conference on
Conference_Location :
Beijing
Print_ISBN :
978-1-4673-1537-1
Type :
conf
DOI :
10.1109/ICCPS.2012.25
Filename :
6197399
Link To Document :
بازگشت