Model checking mobile ad hoc networks

Fatemeh Ghassemi, Wan Fokkink

Research output: Contribution to JournalArticleAcademicpeer-review

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 languageEnglish
Pages (from-to)159-189
Number of pages31
JournalFormal Methods in System Design
Volume49
Issue number3
DOIs
Publication statusPublished - 1 Dec 2016

Fingerprint

Model checking
Mobile ad hoc networks
Mobile Ad Hoc Networks
Model Checking
Multi-hop
Path
Connectivity
Topology
Leader Election
Network protocols
Labeled Transition System
Temporal logic
Network Protocols
Formal Verification
Arbitrary
Violate
Quantifiers
Temporal Logic
Branching
Semantics

Keywords

  • Constrained labeled transition systems
  • Mobile ad hoc networks
  • Model checking
  • Multi-hop network constraints

Cite this

Ghassemi, Fatemeh ; Fokkink, Wan. / Model checking mobile ad hoc networks. In: Formal Methods in System Design. 2016 ; Vol. 49, No. 3. pp. 159-189.
@article{6047cb4373c845dd9dea094e7274f2c3,
title = "Model checking mobile ad hoc networks",
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.",
keywords = "Constrained labeled transition systems, Mobile ad hoc networks, Model checking, Multi-hop network constraints",
author = "Fatemeh Ghassemi and Wan Fokkink",
year = "2016",
month = "12",
day = "1",
doi = "10.1007/s10703-016-0254-7",
language = "English",
volume = "49",
pages = "159--189",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "3",

}

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 JournalArticleAcademicpeer-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 -