Model Checking MANETs with Arbitrary Mobility - Fundamentals of Software Engineering Access content directly
Conference Papers Year : 2013

Model Checking MANETs with Arbitrary Mobility


Modeling arbitrary connectivity changes of mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We introduced constrained labeled transition systems (CLTSs) as a semantic model to represent mobility. To model check MANET protocol with respect to the underlying topology and connectivity changes, we here introduce a branching-time temporal logic interpreted over CLTSs. The temporal operators, from Action Computation Tree Logic with an unless operator, are parameterized by multi-hop constraints over topologies, to express conditions on successful scenarios of a MANET protocol. We moreover provide a bisimilarity relation with the same distinguishing power for CLTSs as our logical framework.
Fichier principal
Vignette du fichier
978-3-642-40213-5_14_Chapter.pdf (404.82 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01514658 , version 1 (26-04-2017)





Fatemeh Ghassemi, Saeide Ahmadi, Wan Fokkink, Ali Movaghar. Model Checking MANETs with Arbitrary Mobility. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.217-232, ⟨10.1007/978-3-642-40213-5_14⟩. ⟨hal-01514658⟩
132 View
35 Download



Gmail Facebook X LinkedIn More