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).
:: 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.