Files in this item



application/pdfwrla14-manets0111.pdf (945kB)
(no description provided)PDF


Title:A Formal Framework for Mobile Ad hoc Networks in Real-Time Maude
Author(s):Liu, Si; Olveczky, Peter C.; Meseguer, José
Subject(s):Mobile ad hoc networks
Real-Time Maude
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.
Issue Date:2017
Genre:Technical Report
Date Available in IDEALS:2017-05-24

This item appears in the following Collection(s)

Item Statistics