State space reduction techniques for model checking of MANET protocols

Abstract

A Mobile Ad hoc Network (MANET) is a network that consists of mobile nodes andis autonomously managed without infrastructure base stations such as accesspoints. MANETs have started being used as part of safety critical applications.A Vehicular Ad hoc Network (VANET) used in automated driving systems is such anexample. In such applications, defects in the network protocol may cause serioussocial problems. Model checking, a state search-based verification technique,has proven to be effective in finding faults in complex system designs, such ascommunication protocols. However it is challenging to apply this technique toMANET protocols, because a MANET can have a number of different networktopologies, thus resulting in the state explosion problem very easily. In this paper we propose a modeling technique to mitigate this problem using the AODVprotocol as a running example.MANET protocols, such as AODV, typically enforce a source node that wishes toestablish a route to the destination to retry the route establishing processsome fixed number of times in face of failures. We show that to model check theprotocol's behavior in these retries it suffices to consider only the lasttrial. The results of experiments using the SPIN model checker showthat using the proposed technique significantly reduced the time and memory usage compared to standard full state exploration and allowed us to model check the protocol with up to five nodes.