Validating communication of a dynamic traffic management system

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.