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.
CITATION STYLE
Liu, S., Ölveczky, P. C., & Meseguer, J. (2015). Formal analysis of leader election in MANETs using real-time maude. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8950, 231–252. https://doi.org/10.1007/978-3-319-15545-6_16
Mendeley helps you to discover research relevant for your work.