Home | deutsch  | Legals | Sitemap | KIT

Virtual Traffic Lights

Virtual Traffic Lights
Contact:Natalya AnTill Neudecker 
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, to appear) as well as a visualization of simulations performed with the VTL protocol. 


  • Download: vtl.zip (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