Abstract
Modeling arbitrary connectivity changes within mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We use constrained labeled transition systems as a semantic model to represent mobility. To model check MANET protocols with respect to the underlying topology and connectivity changes, we introduce a branching-time temporal logic. The path quantifiers are parameterized by multi-hop constraints over topologies, to discriminate the paths over which the temporal behavior should be investigated; the paths that violate the multi-hop constraints are not considered. A model checking algorithm is presented to verify MANETs that allow arbitrary mobility, under the assumption of reliable communication. It is applied to analyze a leader election protocol.
| Original language | English |
|---|---|
| Pages (from-to) | 159-189 |
| Number of pages | 31 |
| Journal | Formal Methods in System Design |
| Volume | 49 |
| Issue number | 3 |
| DOIs | |
| Publication status | Published - 1 Dec 2016 |
Fingerprint
Keywords
- Constrained labeled transition systems
- Mobile ad hoc networks
- Model checking
- Multi-hop network constraints
Cite this
}
Model checking mobile ad hoc networks. / Ghassemi, Fatemeh; Fokkink, Wan.
In: Formal Methods in System Design, Vol. 49, No. 3, 01.12.2016, p. 159-189.Research output: Contribution to Journal › Article › Academic › peer-review
TY - JOUR
T1 - Model checking mobile ad hoc networks
AU - Ghassemi, Fatemeh
AU - Fokkink, Wan
PY - 2016/12/1
Y1 - 2016/12/1
N2 - Modeling arbitrary connectivity changes within mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We use constrained labeled transition systems as a semantic model to represent mobility. To model check MANET protocols with respect to the underlying topology and connectivity changes, we introduce a branching-time temporal logic. The path quantifiers are parameterized by multi-hop constraints over topologies, to discriminate the paths over which the temporal behavior should be investigated; the paths that violate the multi-hop constraints are not considered. A model checking algorithm is presented to verify MANETs that allow arbitrary mobility, under the assumption of reliable communication. It is applied to analyze a leader election protocol.
AB - Modeling arbitrary connectivity changes within mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We use constrained labeled transition systems as a semantic model to represent mobility. To model check MANET protocols with respect to the underlying topology and connectivity changes, we introduce a branching-time temporal logic. The path quantifiers are parameterized by multi-hop constraints over topologies, to discriminate the paths over which the temporal behavior should be investigated; the paths that violate the multi-hop constraints are not considered. A model checking algorithm is presented to verify MANETs that allow arbitrary mobility, under the assumption of reliable communication. It is applied to analyze a leader election protocol.
KW - Constrained labeled transition systems
KW - Mobile ad hoc networks
KW - Model checking
KW - Multi-hop network constraints
UR - http://www.scopus.com/inward/record.url?scp=84982913917&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84982913917&partnerID=8YFLogxK
U2 - 10.1007/s10703-016-0254-7
DO - 10.1007/s10703-016-0254-7
M3 - Article
VL - 49
SP - 159
EP - 189
JO - Formal Methods in System Design
JF - Formal Methods in System Design
SN - 0925-9856
IS - 3
ER -