Abstract:
Traffic flow theory allows us to mathematically describe the behavior of traf fic flow and thus deduce interesting properties for transportation engineers.
Traditionally, traffic flow problems are analyzed by using paper-and-pencil
proof methods, computer-based numerical techniques or computer algebra
systems. However all these methods are error-prone and thus the analysis
cannot be termed as accurate, which poses a serious threat to the safety critical domain of transportation systems. To guarantee the correctness of
the analysis, we propose to use higher-order-logic theorem proving for ana lyzing the traffic flow problems and as a first step in this direction, present
a logical framework for the formal analysis of macroscopic models of traffic
flow. In particular, we present a formalization of some foundational con cepts of macroscopic models, namely density, flow rate, mean speed, relative
occupancy and shockwave using the higher-order-logic theorem prover HOL
Light. To illustrate the practical utilization and effectiveness of the proposed
idea, we perform the formal analysis of a German freeway, including its input output and shockwave analysis by verifying their corresponding properties
using our proposed formalization.
