A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> <> [ ] p <s> The bitstate hashing, or supertrace, technique was introduced in 1987 as a method to increase the quality of verification by reachability analyses for applications that defeat analysis by traditional means because of their size. Since then, the technique has been included in many research verification tools, and was even adopted in some tools that are marketed commercially. It is therefore important that we understand well how and why the method works, what its limitations are, and how it compares with alternative schemes that attempt to solve the same problem. <s> BIB001 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> <> [ ] p <s> We show how to use an interactive theorem prover, HOL, together with a model checker, SPIN, to prove key properties of distance vector routing protocols. We do three case studies: correctness of the RIP standard, a sharp real-time bound on RIP stability, and preservation of loop-freedom in AODV, a distance vector protocol for wireless networks. We develop verification techniques suited to routing protocols generally. These case studies show significant benefits from automated support in reduced verification workload and assistance in finding new insights and gaps for standard specifications. <s> BIB002 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> <> [ ] p <s> 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. <s> BIB003 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> <> [ ] p <s> A sensor network is a set of sensor nodes that communicate by sending messages over wireless links either directly to destination node or indirectly over a sequence of intermediate nodes. Sensor networks are often formed by ad-hoc deployment and utilized for information gathering and processing. Reliable and correct behaviors of such sensor based infrastructures are critical for many applications. The goal of this paper is to demonstrate applicability of finite model-checking to analysis and verification of sensor networks specifications modeled as dynamically changing graphs where connections and disconnections are determined by the distance between nodes. <s> BIB004 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> <> [ ] p <s> We present an improved method for analyzing route establishment in ad hoc routing protocols. An efficient abstraction for Propagating Localized Broadcast with Dampening (PLBD) is developed. Applying this result we are able to verify networks and topology changes for ad hoc networks up to the limits currently envisaged for operational mobile ad hoc networks (MANETS). Results are reported for route discovery in the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) using UPPAAL and we provide an outline of how similar verifications can be conducted for DSR. <s> BIB005
where p denotes all channels are empty, i.e., possibly converge. <> [ ] q where q denotes some channels are not empty, i.e., possibly never converge. In words, the first formula specifies that the protocol will possibly converge in the future, i.e., formally, after some A B D Figure 1 : A Simple 3-Node Network time in the future of any execution, for all the succeeding states, it always holds that all channels are empty. Similarly, the second formula specifies that the protocol will possibly never converge in the future. The results of the verifications of the two formulas can help draw a conclusion whether a BGP network configuration will guarantee convergence for a particular network destination. Note that it is hard to generalize this approach to large networks due to the state explosion problem, and also dynamic topology changes are not addressed in the work. A model of AODV protocol was created using Promela in SPIN (302 lines of code), and it was attempted to prove loop-freedom for a simple 3-node network BIB002 4 . The network consists of three nodes, A, B and D, as shown in Fig. 1 . The node A has an active link to B, and B has an active link to D. Both A and B want to send data to the only destination D. The link B-D is fragile and may be broken at any time. In the model, (1) The process type of AODV protocol is instantiated as three processes running at the three nodes. The timeout events are modeled as nondeterministic events that can occur at any time (in fact, it is an over-approximation), since Promela has no notion of real time. (2) The connectivity of the topology is hard-coded as a connection process running in parallel that captures all sent messages and delivers them when appropriate. (3) Broadcasting messages are captured by the process, which then delivers these messages to the sender's neighbors immediately. For such a fixed small topology, hard-coding has significant performance advantages in SPIN. (4) The fragility of the B-D link is modeled as an environment process which can nondeterministically send link-broken events to both B and D at any time. The property to verify is that there cannot be a routing loop between A and B, for any sequence of events. The following LTL formula expresses the loop-free property: In words, for all the states in any execution, it is should never occur that the next pointers of A and B for the destination D point to each other. By running SPIN, a number of counterexamples are found and guide the revision of the draft of the protocol (version 2). The design and model of the protocol are modified several times until SPIN cannot find a loop. Note that SPIN cannot be sure that the fixed protocol will produce no loops for any network, since we only considered a 3-node network rather than unbounded nodes. However, it may indicate that we have found a possibly loop-free solution.  All the codes used in BIB002 are available at http://www.cis.upenn.edu/verinet/RoutingVerification It is also suggested to model each node as a process in BIB004 . These processes manage their own connectivity to other nodes, and also the communication functions. Furthermore, a Location Manager (LM) process is specified to generate topology changes. That is, it nondeterministically decides when and what sensors change their locations and their connectivity to other nodes. The location manager process supports the following activities 5 : • dynamic creation of new nodes, i.e., new processes. • dynamic deletion of nodes, i.e., disconnection or termination of processes. • dynamic creation of new edges, i.e., new connection. • dynamic deletion of edges, i.e., disconnection between two nodes. Node processes listen to LM, and adjust their connectivity with other nodes based on received messages from LM. Note that this modeling approach can only be used on small networks containing finite nodes, due to the state explosion problem. In some other works, it is also admitted that the state explosion problem is a key impedient of model checking routing protocols due to mobility of nodes. Therefore, people only considered and modeled a five node network including a sender, a receiver and three intermediates in BIB003 . A lot of restrictions on the model configurations have been imposed to obtain a simplified basic model, e.g., limiting the number of possible links of each node, constraints on the possible topologies, etc. These simplifications can significantly reduce the state space in checking, but may also greatly reduce the confidence of the result. In the model, (1) Each node is modeled as a process of simplified protocol. (2) The connectivity is saved in the routing table of each node. (3) Each node X has a channel braodcastX only through which it can receive messages. The broadcasting operation is coded into each process to send messages to connected neighbors. (4) Node mobility is realized by canceling all routing table entries of the moving node, and setting a new link initialization for this node. One shortcoming of this method is extensibility. If we want to extend the verification to the models containing more nodes, more efforts are required to modify the code. Based on the established basic model, the properties of deadlock and loop-freedom are checked. However, as we mentioned, due to the limited number of nodes and the restrictions on the configurations (e.g., possible links and topologies), the verification result is not trustable enough. It is also suggested that, when checking on large networks, SPIN can be used in the supertrace mode with the bitstate hashing technique BIB001 to save memory, with the cost of slightly reducing the coverage to about 98% BIB003 . A general model of LUNAR was created using Promela in SPIN (about 250 lines of code excluding comments)  BIB005 . In the model, (1) Each node is a process instantiating the process type of a simplified version of LUNAR, where communication ports are modeled as channels stored in an array indexed by node id. (2) Connectivity is modeled as a symmetric, two dimensional array of booleans. The matrix is symmetric since the protocol assumes bidirectional connections. (3) Broadcast is modeled by unicasting to all nodes with whom the sending node has connectivity at that time. The unicast operations consisting a broadcast are implemented atomically to ensure its atomicity. (4) Topology changes are modeled using a separate process, which can modify the global connectivity matrix at any time. In the verification, only one source and one destination are selected. The topology and node transitions are also selected, so that the two nodes are always connected. A hop counter is defined to keep track of the number of nodes traversed by the packet before it reaches its destination. Based on the model, the properties of deadlock and loopfreedom are checked. Loop-freedom is formalized as the assertion: a packet does not traverse more nodes than theoretically possible before the packet reaches its destination. Absence of deadlock is formalized as a liveness property such that the packet will eventually be delivered in the future. Their first verification attempt is to generate nondeterministically a topology for a given number of nodes, then the protocol is verified on each generated topology. Thus, all possible topologies are considered. However, the state space is too large to be efficiently checked. When node mobility is added, an exhaustive search is no longer feasible even for a small number of nodes. Therefore, their second attempt focuses on a few typical scenarios (containing four or five nodes, and once or twice simple topology changes) which seem to cause problems for the protocol. The bitstate hashing option is not used in the verification to ensure reliable result. The checker cannot exhaustively search all the states when there are more than five nodes due to the memory limit of 36GB.