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
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, April 26, 2017 - 3:21:57 PM
Last modification on : Friday, January 7, 2022 - 12:00:02 PM
Long-term archiving on: : Thursday, July 27, 2017 - 1:12:45 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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⟩



Record views


Files downloads