Skip to main content
Department of Information Technology

SPIN and UPPAAL ad hoc routing protocol models

Below is a list of ad hoc routing protocol models verified using SPIN and UPPAAL.

LUNAR SPIN models Description Model File Property File
LUNAR model (4 nodes, 1 down) SPIN model corresponding to scenario (a) in FORTE'04 and FORTE'05 papers .pml file .aut file
LUNAR model (4 nodes, 1 up) SPIN model corresponding to scenario (b) in FORTE'04 and FORTE'05 papers .pml file .aut file
LUNAR model (4 nodes, simul. 1) SPIN model corresponding to scenario (c) in FORTE'04 and FORTE'05 papers .pml file .aut file
LUNAR model (4 nodes, 1 down and up) SPIN model corresponding to scenario (d) in FORTE'04 and FORTE'05 papers .pml file .aut file
LUNAR model (5 nodes, 1 up) SPIN model corresponding to scenario (f) in FORTE'04 and FORTE'05 papers .pml file .aut file

The LUNAR SPIN models corresponding to scenarios (e), (g), and (h) in the FORTE papers are just straightforward variants of the above models (different topology changes and channel capacities).

LUNAR UPPAAL models Description Model File Property File
LUNAR model (4 nodes, 1 down) UPPAAL model corresponding to scenario (a) in FORTE'04 and FORTE'05 papers .xml file .q file
LUNAR model (4 nodes, 1 up) UPPAAL model corresponding to scenario (b) in FORTE'04 and FORTE'05 papers .xml file .q file
LUNAR model (4 nodes, simul. 1) UPPAAL model corresponding to scenario (c) in FORTE'04 and FORTE'05 papers .xml file .q file
LUNAR model (4 nodes, 1 down and up) UPPAAL model corresponding to scenario (d) in FORTE'04 and FORTE'05 papers .xml file .q file
LUNAR model (5 nodes, 1 down) UPPAAL model corresponding to scenario (e) in FORTE'04 and FORTE'05 papers .xml file .q file
LUNAR model (5 nodes, 1 up) UPPAAL model corresponding to scenario (f) in FORTE'04 and FORTE'05 papers .xml file .q file
LUNAR model (6 nodes, 1 down) UPPAAL model corresponding to scenario (g) in FORTE'04 and FORTE'05 papers .xml file .q file
LUNAR model (7 nodes, 1 down) UPPAAL model corresponding to scenario (h) in FORTE'04 and FORTE'05 papers .xml file .q file

The models above have been converted to UPPAAL 4.0.6 syntax.

Message centered UPPAAL models Description Model File Property File
LUNAR model (3 min, 3 max, 1 breaks) UPPAAL model for network with minimum and maximum hop distances between source and destination set to 3 and one link break permitted. .xml file .q file

The model above has been converted to UPPAAL 4.0.6 syntax.

Updated  2016-08-17 15:26:29 by Björn Victor.