Towards Formal Verification of Macroscopic Models in Traffic Flow Theory
Traditionally, traffic flow analysis is led using data collection and simulation-based validation. As traffic infrastructure is becoming more interconnected and automated, relying on the best effort of simulation-based validation can be inefficient to identify anomalies that degrade the mobility and safety requirements of the transportation network. Higher-order-logic theorem proving is a formal method that can overcome coverage limitations of simulation-based methods and its soundness can guarantees correctness of the results. Therefore, we propose to use higher-order-logic theorem proving for analyzing fundamental traffic flow problems and, as the first step in this direction, we present a logical framework for the formal analysis of macroscopic models of traffic flow. Leveraging upon the high expressiveness of the underlying logic, we formally model the continuous components of macroscopic models while capturing their real behavior. In particular, we present a formalization of some foundation concepts of macroscopic models, namely density, flow rate, mean speed, relative occupancy, and shockwave using the higher-order-logic theorem prover HOL Light. This choice is primarily motivated by the fact that the macroscopic models play a vital role in planning strategies in allocating resources for implementing optimized and balanced transportation systems. For illustration, we perform the formal input-output and shockwave analysis of a German freeway.