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.
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
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⟩