Formal Modeling and Analysis of Leader Election in MANETs

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

Permalink

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

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

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

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