MODELNG THE AODV ROUTING PROTOCOL IN THE ω-CALCULUS

Mobile ad hoc wireless networks (MANETs) are autonomous collections of mobile nodes that communicate over wireless links. Formal verification of routing protocols for MANETs requires concise yet property-preserving modeling to correctly verify the model and at the same time also avoid running into the problem of state-space explosion. The characteristics of MANETs that pose challenge to the task of modeling are node mobility and broadcast. We have developed a new modeling formalism, called the ω-calculus, to naturally and succinctly model MANET protocols. This paper describes the modeling of AODV, a reactive routing protocol for MANETs, in the ω-calculus. We aim to subject the model to formal verification in order to prove properties of the AODV routing protocol.