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
AN - SCOPUS:84982913917
VL - 49
SP - 159
EP - 189
JO - Formal Methods in System Design
JF - Formal Methods in System Design
SN - 0925-9856
IS - 3
ER -