Virtual Traffic Lights

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.



  • Download: (The zip file contains the used PROMELA model and the sources for the performed ns-3 simulations).
The PROMELA VTL model can be used for verification with the SPIN model checker . The following excerpt gives an example of the PROMELA VTL model and shows the method that is used to check, whether the consensus invariant (Section IV-B) holds true.
inline checkAssert()
d_step {
:: i >= NPROC -> break
:: else ->
:: (tgreen == 255 && greenRoad[i] != 255) -> tgreen = greenRoad[i]
:: else
assert(greenRoad[i] == tgreen || greenRoad[i] == 255);
The method iterates through all processes (i.e., vehicles) and checks, whether the traffic light signal set (stored as the road with a greenlight in greenRoad[]) is the same for all vehicles. Vehicles are allowed to have an invalid traffic light signal set as well (i.e., greenRoad[i] == 255), as they perform a fallback approach in that case. For further details, plrease refer to the model source code.

VTL Visualization

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.
Please note: A recent, HTML5 capable browser is required to view the visualization.

Protocol State
Approach State
Time ID Message