Automatized Verification of Ad Hoc Routing Protocols

Numerous specialized ad hoc routing protocols are currently proposed for use, or being implemented. Few of them have been subjected to formal verification. This paper evaluates two model checking tools, SPIN and UPPAAL, using the verification of the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) as a case study. Insights are reported in terms of identifying important modeling considerations and the types of ad hoc protocol properties that can realistically be verified.

• Type: Conference
• Year: 2004
• Where: FORTE
• Authors: Oskar Wibling, Joachim Parrow, Arnold Neville Pears
• Keywords: Ad Hoc Protocol, Ad Hoc Routing Protocol, FORTE 2004, FORTE 2007, Network Ad Hoc