TY - JOUR
T1 - Formal analysis of leader election in MANETs using real-time maude
AU - Liu, Si
AU - Ölveczky, Peter Csaba
AU - Meseguer, José
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2015
Y1 - 2015
N2 - The modeling and analysis of mobile ad hoc networks (MANETs) pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectionality can interact in unforeseen ways that are hard tomodel and analyze by automatic formal methods. In this work we use rewriting logic and Real- Time Maude to address this challenge. We propose a composable formal framework for MANET protocols and their mobility models that can take into account such complex interactions. We illustrate our framework by analyzing awell-studied leader election protocol for MANETs in the presence of both mobility and uni- and bidirectional links.
AB - The modeling and analysis of mobile ad hoc networks (MANETs) pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectionality can interact in unforeseen ways that are hard tomodel and analyze by automatic formal methods. In this work we use rewriting logic and Real- Time Maude to address this challenge. We propose a composable formal framework for MANET protocols and their mobility models that can take into account such complex interactions. We illustrate our framework by analyzing awell-studied leader election protocol for MANETs in the presence of both mobility and uni- and bidirectional links.
UR - http://www.scopus.com/inward/record.url?scp=84924358443&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84924358443&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-15545-6_16
DO - 10.1007/978-3-319-15545-6_16
M3 - Article
AN - SCOPUS:84924358443
SN - 0302-9743
VL - 8950
SP - 231
EP - 252
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -