%0 Conference Proceedings
%T Model Checking MANETs with Arbitrary Mobility
%+ University of Tehran
%+ Vrije Universiteit Amsterdam [Amsterdam] (VU)
%+ Sharif University of Technology [Tehran] (SUT)
%A Ghassemi, Fatemeh
%A Ahmadi, Saeide
%A Fokkink, Wan
%A Movaghar, Ali
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 5th International Conference on Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Farhad Arbab
%Y Marjan Sirjani
%I Springer Berlin Heidelberg
%3 Fundamentals of Software Engineering
%V LNCS-8161
%P 217-232
%8 2013-04-24
%D 2013
%R 10.1007/978-3-642-40213-5_14
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%2 https://inria.hal.science/hal-01514658/document
%2 https://inria.hal.science/hal-01514658/file/978-3-642-40213-5_14_Chapter.pdf
%L hal-01514658
%U https://inria.hal.science/hal-01514658
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ IFIP-LNCS-8161