Correctness Proof for a Dynamic Adaptive Routing Algorithm for Mobile Ad-hoc Networks

Correctness Proof for a Dynamic Adaptive Routing Algorithm for Mobile Ad-hoc Networks

Title : Correctness Proof for a Dynamic Adaptive Routing Algorithm for Mobile Ad-hoc Networks
Authors :
Yang, Shahan
Baras, John, S.
Conference : IFAC Workshop – Modeling and Analysis of Logic Controlled Dynamic Systems pp. 1-10
Date: July 30 - August 01, 2003

Dynamic and adaptive routing algorithms are the “brains” of mobile ad-hoc networks (MANETs), in that they govern the self-organization of these networks. MANETs are infrastructureless “intelligent” networks, which are becoming increasingly popular and have wide applicability. In this paper, we view dynamic adaptive routing algorithms for MANETs as hybrid systems (partly based on logic and partly based on numerics). In this paper, we introduce formal models for the analysis and verification of one such routing algorithm, the Temporally Oriented Routing Algorithm (TORA) under certain assumptions. More specifically we give a rigorous mathematical proof of correctness and convergence of TORA. Other formal methods, their limitations and future research challenges are also discussed.