University of Illinois Urbana-Champaign

Formal Modeling and Analysis of Leader Election in MANETs

Liu, Si; Olveczky, Peter C.; Meseguer, José

Content Files
main.pdf

Permalink

https://hdl.handle.net/2142/96169

Description

Title
Formal Modeling and Analysis of Leader Election in MANETs
Author(s)
  • Liu, Si
  • Olveczky, Peter C.
  • Meseguer, José
Issue Date
2015
Keyword(s)
  • Mobile ad hoc networks
  • Real-Time Maude
  • Leader Election
  • Mobility
  • Model Checking
Date of Ingest
2017-05-24T15:49:15Z
Abstract
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 to model 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 a well-studied leader election protocol for MANETs in the presence of both mobility and uni- and bidirectional links.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/96169
Sponsor(s)/Grant Number(s)
  • NSF Grant CNS 13-19109
  • AFOSR Grant FA8750-11-2-0084

Owning Collections

Research and Tech Reports - Computer Science PRIMARY