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.
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.
:: i >= NPROC -> break
:: else ->
:: (tgreen == 255 && greenRoad[i] != 255) -> tgreen = greenRoad[i]
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.
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.