Mobile ad hoc networks (MANETs) are wireless networks formed spontaneously. Communication in such networks typically involves multi-hop relays, and is subjected to dynamic topology changes and frequent link failures. This complex scenario demands robust routing protocol standards that ensure correct and timely delivery of messages. Recently, formal verification has been successful in detecting ambiguities in protocol standards. We consider the Ad hoc On Demand Distance Vector (AODV) protocol, a reactive protocol currently undergoing standardisation at the IETF (RFC3561). AODV performs route discovery whenever a route to the destination is needed, and retains routing information for a period of time specified by the standard. We apply the real-time model checker UPPAAL to consider the effect of the protocol parameters on the timing behaviour of AODV, thus complementing the earlier untimed verification effort. Our study of the recent versions of the standard (RFC3561-bis-01) has highlighted a dependency of the lifetime of routes on network size, which can be alleviated by allowing the route timeouts to adapt to network growth.
展开▼
