Validating communication of a dynamic traffic management system

Jeroen Verbakel; Wan Fokkink; Joanna Van De Mortel-Fronczak; Jacobus Rooda

doi:10.1109/ICECCS59891.2023.00033

Validating communication of a dynamic traffic management system

Jeroen Verbakel^*
, Wan Fokkink
, Joanna Van De Mortel-Fronczak
, Jacobus Rooda

^*Corresponding author for this work

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

49 Downloads (Pure)

Abstract

With the increasing traffic density on highways, maintaining the safety of road users is imperative. To this end, dynamic traffic management is used. The dynamic traffic management system in the Netherlands comprises roadside units along the highways and traffic control centers where operators monitor and control the traffic. Since highways are geographically spread out, this system is inherently distributed, with a network between the roadside units and traffic control centers. In this paper, application of formal methods to this real, large scale system is discussed. The protocol used for this network is modeled using the algebra of communicating processes (ACP). Furthermore, desirable properties of the protocol are captured in modal μ-calculus formulae. These formulae are verified for the model using the mCRL2 toolchain. Through this formal verification, it is shown that the protocol is sound and functions as intended.

Original language	English
Title of host publication	2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS)
Subtitle of host publication	[Proceedings]
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	207-215
Number of pages	9
ISBN (Electronic)	9798350340044
ISBN (Print)	9798350340051
DOIs	https://doi.org/10.1109/ICECCS59891.2023.00033
Publication status	Published - 2023
Event	27th International Conference on Engineering of Complex Computer Systems, ICECCS 2023 - Toulouse, France Duration: 14 Jun 2023 → 16 Jun 2023

Publication series

Name	Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
ISSN (Print)	2770-8527
ISSN (Electronic)	2770-8535

Conference

Conference	27th International Conference on Engineering of Complex Computer Systems, ICECCS 2023
Country/Territory	France
City	Toulouse
Period	14/06/23 → 16/06/23

Bibliographical note

Publisher Copyright:
© 2023 IEEE.

Keywords

communication protocol
formal verification
traffic management

Access to Document

10.1109/ICECCS59891.2023.00033

Validating_communication_of_a_dynamic_traffic_management_systemFinal published version, 996 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

Verbakel, J., Fokkink, W., Van De Mortel-Fronczak, J., & Rooda, J. (2023). Validating communication of a dynamic traffic management system. In 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS): [Proceedings] (pp. 207-215). (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICECCS59891.2023.00033

Verbakel, Jeroen ; Fokkink, Wan ; Van De Mortel-Fronczak, Joanna et al. / Validating communication of a dynamic traffic management system. 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS): [Proceedings]. Institute of Electrical and Electronics Engineers Inc., 2023. pp. 207-215 (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS).

@inproceedings{243e7f0103bd4b709dc510b2e80d752b,

title = "Validating communication of a dynamic traffic management system",

abstract = "With the increasing traffic density on highways, maintaining the safety of road users is imperative. To this end, dynamic traffic management is used. The dynamic traffic management system in the Netherlands comprises roadside units along the highways and traffic control centers where operators monitor and control the traffic. Since highways are geographically spread out, this system is inherently distributed, with a network between the roadside units and traffic control centers. In this paper, application of formal methods to this real, large scale system is discussed. The protocol used for this network is modeled using the algebra of communicating processes (ACP). Furthermore, desirable properties of the protocol are captured in modal μ-calculus formulae. These formulae are verified for the model using the mCRL2 toolchain. Through this formal verification, it is shown that the protocol is sound and functions as intended.",

keywords = "communication protocol, formal verification, traffic management",

author = "Jeroen Verbakel and Wan Fokkink and \{Van De Mortel-Fronczak\}, Joanna and Jacobus Rooda",

note = "Publisher Copyright: {\textcopyright} 2023 IEEE.; 27th International Conference on Engineering of Complex Computer Systems, ICECCS 2023 ; Conference date: 14-06-2023 Through 16-06-2023",

year = "2023",

doi = "10.1109/ICECCS59891.2023.00033",

language = "English",

isbn = "9798350340051",

series = "Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "207--215",

booktitle = "2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS)",

address = "United States",

}

Verbakel, J, Fokkink, W, Van De Mortel-Fronczak, J & Rooda, J 2023, Validating communication of a dynamic traffic management system. in 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS): [Proceedings]. Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS, Institute of Electrical and Electronics Engineers Inc., pp. 207-215, 27th International Conference on Engineering of Complex Computer Systems, ICECCS 2023, Toulouse, France, 14/06/23. https://doi.org/10.1109/ICECCS59891.2023.00033

Validating communication of a dynamic traffic management system. / Verbakel, Jeroen; Fokkink, Wan; Van De Mortel-Fronczak, Joanna et al.
2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS): [Proceedings]. Institute of Electrical and Electronics Engineers Inc., 2023. p. 207-215 (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS).

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

TY - GEN

T1 - Validating communication of a dynamic traffic management system

AU - Verbakel, Jeroen

AU - Fokkink, Wan

AU - Van De Mortel-Fronczak, Joanna

AU - Rooda, Jacobus

PY - 2023

Y1 - 2023

N2 - With the increasing traffic density on highways, maintaining the safety of road users is imperative. To this end, dynamic traffic management is used. The dynamic traffic management system in the Netherlands comprises roadside units along the highways and traffic control centers where operators monitor and control the traffic. Since highways are geographically spread out, this system is inherently distributed, with a network between the roadside units and traffic control centers. In this paper, application of formal methods to this real, large scale system is discussed. The protocol used for this network is modeled using the algebra of communicating processes (ACP). Furthermore, desirable properties of the protocol are captured in modal μ-calculus formulae. These formulae are verified for the model using the mCRL2 toolchain. Through this formal verification, it is shown that the protocol is sound and functions as intended.

AB - With the increasing traffic density on highways, maintaining the safety of road users is imperative. To this end, dynamic traffic management is used. The dynamic traffic management system in the Netherlands comprises roadside units along the highways and traffic control centers where operators monitor and control the traffic. Since highways are geographically spread out, this system is inherently distributed, with a network between the roadside units and traffic control centers. In this paper, application of formal methods to this real, large scale system is discussed. The protocol used for this network is modeled using the algebra of communicating processes (ACP). Furthermore, desirable properties of the protocol are captured in modal μ-calculus formulae. These formulae are verified for the model using the mCRL2 toolchain. Through this formal verification, it is shown that the protocol is sound and functions as intended.

KW - communication protocol

KW - formal verification

KW - traffic management

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

UR - https://www.scopus.com/pages/publications/85179516370#tab=citedBy

U2 - 10.1109/ICECCS59891.2023.00033

DO - 10.1109/ICECCS59891.2023.00033

M3 - Conference contribution

AN - SCOPUS:85179516370

SN - 9798350340051

T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS

SP - 207

EP - 215

BT - 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS)

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 27th International Conference on Engineering of Complex Computer Systems, ICECCS 2023

Y2 - 14 June 2023 through 16 June 2023

ER -

Verbakel J, Fokkink W, Van De Mortel-Fronczak J, Rooda J. Validating communication of a dynamic traffic management system. In 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS): [Proceedings]. Institute of Electrical and Electronics Engineers Inc. 2023. p. 207-215. (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS). Epub 2023 Nov 22. doi: 10.1109/ICECCS59891.2023.00033

Validating communication of a dynamic traffic management system

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this