Formal verification of ad-hoc routing protocols using SPIN model checker

Tests and simulations are the only verification techniques used for ad-hoc network routing protocols. Although these techniques give us an excellent overview of the protocol behavior, some undesirable aspects of the protocol could still be undiscovered. Therefore formal verification is needed. This paper presents a new technique to formally verify such protocols by the use of a well-known model-checker: SPIN. As an example, a formal verification of the wireless adaptive routing protocol (W.A.R.P) has been performed.