| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [27 references]
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
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