A Formal Framework for Mobile Ad hoc Networks in Real-Time Maude

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

Permalink

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

Description

Title

A Formal Framework for Mobile Ad hoc Networks in Real-Time Maude

Author(s)

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

Issue Date

2017

Keyword(s)

• Mobile ad hoc networks
• Real-Time Maude
• Mobility
• AODV
• Model Checking

Abstract

Mobile ad hoc networks (MANETs) are increasingly popular and deployed in a wide range of environments. However, it is challenging to formally analyze a MANET, both because there are few reasonably accurate formal models of mobility, and because the large state space caused by the movements of the nodes renders straight-forward model checking hard. In particular, the combination of wireless communication and node movement is subtle and does not seem to have been adequately addressed in previous formal methods work. This paper presents a formal executable and parameterized modeling framework for MANETs in Real-Time Maude that integrates several mobility models and wireless communication. We illustrate the use of our modeling framework with the Ad hoc On-Demand Distance Vector (AODV) routing protocol, which allows us to analyze this protocol under different mobility models.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/96163

Owning Collections