With increasing urbanization and motorization, traffic congestion in urban areas becomes a more and more challenging problem. Vehicular Ad-Hoc Network (VANET) enabled Virtual Traffic Lights (VTL) are envisioned to mitigate congestion by eliminating the need for infrastructure based traffic lights and increasing the efficiency by up to 60% (Ferreira et al., 2010).
This page provides the PROMELA VTL model as used in Verification and Evaluation of Fail-Safe Virtual Traffic Light Applications (IEEE VNC 2013) as well as a visualization of simulations performed with the VTL protocol.
PROMELA VTL Model
- Download: vtl.zip (The zip file contains the used PROMELA model and the sources for the performed ns-3 simulations).
:: i >= NPROC -> break
:: else ->
:: (tgreen == 255 && greenRoad[i] != 255) -> tgreen = greenRoad[i]
assert(greenRoad[i] == tgreen || greenRoad[i] == 255);
The visualization shows vehicles equipped with VTL traversing a Manhattan Grid. It also lists diagnostic output generated by the VTL algorithm.
- Select the intersection management control method from the dropdown box. (Loading the trace file may take some time.)
- Select whether the vehicle's color should indicate a) speed, b) protocol state (e.g., VTL Leader) or c) approach state (e.g., red, green).
- Press Play to watch the visualization.
- When pausing the visualization, move the mouse over vehicles to get additional information or click on a trace message below to jump to the emitting vehicle.