Towards formal verification of freeway traffic control

Stefan Mitsch; Sarah M. Loos; Andre Platzer

doi:10.1109/ICCPS.2012.25

Towards formal verification of freeway traffic control

Stefan Mitsch
, Sarah M. Loos
, Andre Platzer

Department of Cooperative Information Systems

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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.

Original language	English
Title of host publication	Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems (ICCPS '12)
Editors	Chenyang Lu
Place of Publication	Washington, DC, USA
Publisher	IEEE Computer Society
Pages	171-180
Number of pages	10
ISBN (Print)	978-0-7695-4695-7
DOIs	https://doi.org/10.1109/ICCPS.2012.25
Publication status	Published - 2012

Fields of science

102 Computer Sciences
102006 Computer supported cooperative work (CSCW)
102015 Information systems
102014 Information design
102027 Web engineering

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.1109/ICCPS.2012.25

Cite this

@inproceedings{d34c6901545f4a18ac312c2d05f72ce2,

title = "Towards formal verification of freeway traffic control",

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.",

author = "Stefan Mitsch and Loos, \{Sarah M.\} and Andre Platzer",

year = "2012",

doi = "10.1109/ICCPS.2012.25",

language = "English",

isbn = "978-0-7695-4695-7",

pages = "171--180",

editor = "\{Chenyang Lu\}",

booktitle = "Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems (ICCPS '12)",

publisher = "IEEE Computer Society",

}

Towards formal verification of freeway traffic control. / Mitsch, Stefan; Loos, Sarah M.; Platzer, Andre.
Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems (ICCPS '12). ed. / Chenyang Lu. Washington, DC, USA: IEEE Computer Society, 2012. p. 171-180 6197399.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Towards formal verification of freeway traffic control

AU - Mitsch, Stefan

AU - Loos, Sarah M.

AU - Platzer, Andre

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84861509153

U2 - 10.1109/ICCPS.2012.25

DO - 10.1109/ICCPS.2012.25

M3 - Conference proceedings

SN - 978-0-7695-4695-7

SP - 171

EP - 180

BT - Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems (ICCPS '12)

A2 - Chenyang Lu, null

PB - IEEE Computer Society

CY - Washington, DC, USA

ER -

Towards formal verification of freeway traffic control

Abstract

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this