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).
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=0;
tgreen=255;
do
:: i >= NPROC -> break
:: else ->
if
:: (tgreen == 255 && greenRoad[i] != 255) -> tgreen = greenRoad[i]
:: else
fi;
assert(greenRoad[i] == tgreen || greenRoad[i] == 255);
i++
od;
i=0;
tgreen=255
}
}
{
d_step {
i=0;
tgreen=255;
do
:: i >= NPROC -> break
:: else ->
if
:: (tgreen == 255 && greenRoad[i] != 255) -> tgreen = greenRoad[i]
:: else
fi;
assert(greenRoad[i] == tgreen || greenRoad[i] == 255);
i++
od;
i=0;
tgreen=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.
Speed
Protocol State
Approach State
Protocol State
Approach State
| Time | ID | Message |