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.