Skip to Main content Skip to Navigation
Conference papers

Model Checking MANETs with Arbitrary Mobility

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01514658
Contributor : Hal Ifip <>
Submitted on : Wednesday, April 26, 2017 - 3:21:57 PM
Last modification on : Monday, September 24, 2018 - 3:30:02 PM
Long-term archiving on: : Thursday, July 27, 2017 - 1:12:45 PM

File

978-3-642-40213-5_14_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

222

Files downloads

187