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.