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. © 2013 IFIP International Federation for Information Processing.
Cite
CITATION STYLE
Ghassemi, F., Ahmadi, S., Fokkink, W., & Movaghar, A. (2013). Model checking MANETs with arbitrary mobility. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8161 LNCS, pp. 217–232). Springer Verlag. https://doi.org/10.1007/978-3-642-40213-5_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
