Abstract

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.

Framework

Proof Script

• Proof Script

Student

Muhammad Umair is a MS student at the Research Center for Modeling and Simulation of National University of Sciences and Technology. He is working on his MS thesis in the System Analysis & Verification (SAVe) Lab of NUST-SEECS, under the supervision of Dr. Osman Hasan.