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.
Type de document :
Communication dans un congrès
Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.217-232, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_14〉
https://hal.inria.fr/hal-01514658
Contributeur : Hal Ifip
<>
Soumis le : mercredi 26 avril 2017 - 15:21:57
Dernière modification le : vendredi 2 mars 2018 - 15:04:02
Document(s) archivé(s) le : jeudi 27 juillet 2017 - 13:12:45
Fatemeh Ghassemi, Saeide Ahmadi, Wan Fokkink, Ali Movaghar. Model Checking MANETs with Arbitrary Mobility. Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.217-232, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_14〉. 〈hal-01514658〉
