A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Overview <s> This document specifies a routing protocol, based on the Routing ::: Information Protocol (RIP), as defined in [1,2], for the Simple ::: Internet Protocol (SIP), as defined in [3]. A companion document will ::: define the SNMP MIB objects for SIP-RIP (TBD). <s> BIB001 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Overview <s> This document specifies an extension of the Routing Information Protocol (RIP), as defined in [1,2], to expand the amount of useful information carried in RIP messages and to add a measure of security. This memo obsoletes RFC 1388, which specifies an update to the "Routing Information Protocol" STD 34, RFC 1058. <s> BIB002 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Overview <s> Part I. Tutorial: 1. Introduction to ML 2. The HOL logic 3. Introduction to proof with HOL 4. Goal-oriented proof: tactics and tacticals 5. Example: a simple parity checker 6. How to program a proof tool 7. Example: the binomial theorem Part II. The Meta-Language ML: 8. The history of ML 9. Introduction and examples 10. Syntax of ML 11. Semantics of ML 12. ML types 13. Primitive ML identifier bindings 14. General purpose and list processing functions 15. ML system functions Part III. The Hol Logic: 16. Syntax and semantics 17. Theories Part IV. The Hol System: 18. The HOL logic in ML Part V. Theorem-Proving With HOL: 19. Derived inference rules 20. Conversions 21. Goal-directed proof: tactics and tacticals Appendices. <s> BIB003 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Overview <s> An ad-hoc network is the cooperative engagement of a collection of mobile nodes without the required intervention of any centralized access point or existing infrastructure. We present Ad-hoc On Demand Distance Vector Routing (AODV), a novel algorithm for the operation of such ad-hoc networks. Each mobile host operates as a specialized router, and routes are obtained as needed (i.e., on-demand) with little or no reliance on periodic advertisements. Our new routing algorithm is quite suitable for a dynamic self starting network, as required by users wishing to utilize ad-hoc networks. AODV provides loop-free routes even while repairing broken links. Because the protocol does not require global periodic routing advertisements, the demand on the overall bandwidth available to the mobile nodes is substantially less than in those protocols that do necessitate such advertisements. Nevertheless we can still maintain most of the advantages of basic distance vector routing mechanisms. We show that our algorithm scales to large populations of mobile nodes wishing to form ad-hoc networks. We also include an evaluation methodology and simulation results to verify the operation of our algorithm. <s> BIB004 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Overview <s> From the Publisher: ::: Provides a simple and clear presentation, covering propositional and predicate logic and some specialized logics used for reasoning about the correctness of computer systems. <s> BIB005 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Overview <s> In this paper we describe LUNAR, a lean and efficient routing protocol for wireless ad hoc networks. We report on its implementation, on performance comparisons and on a formal validation result. T ... <s> BIB006
We should consider two things when applying formal verification to ad hoc routing protocols. First, we need to specify the key properties that should be satisfied by protocols, and then choose appropriate tools to formally model systems and verify these properties. Second, we should carefully use appropriate verification techniques to deal with the state explosion problem, and optimize our techniques with respect to two factors: the unbounded number of nodes and the large number of possible topologies for a given number of nodes. This paper is organized as follows. The tools for verification are briefly introduced in Section 2. The key properties that are expected to satisfy are described in Section 3. The two classes of formal verification techniques are reviewed in Section 4. We discuss challenges and future work in Section 5, and conclude in Section 6. The case studies in this paper concern the Border Gateway Protocol (BGP)   which is the principal exterior gateway protocol, and the protocols for interior gateway such as the Routing Information Protocol (RIP) BIB001 BIB002 BIB002 which is a table-driven distance vector routing protocol using the asynchronous distributed Bellman-Ford protocol, the Ad hoc On-Demand Distance Vector (AODV) routing protocol BIB004  , and the Lightweight Underlay Network Ad-Hoc Routing Protocol (LUNAR) BIB006 which is a simplified AODV-like protocol. execution, SPIN will provide a counterexample to aid fault diagnosis and revision of the system. The UPPAAL model checker  is an integrated tool environment for modeling, validation and verification of realtime systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.) and channel synchronization. A system is modeled using timed automata which are drawn in a graphical user interface, while a property is specified as a CTL (Computation Tree Logic BIB005 ) formula. UPPAAL contains also a simulator and a checker. The verification process is fully automatic, and provides a counterexample if the property is violated in some execution. The HOL theorem prover system BIB003 is a general purpose verification environment based on Higher-Order Logic. A system is modeled as functions using a functional programming language, while a property is specified using higherorder logic. HOL uses a proof assistant that allows the user to construct proofs of such properties by using certain proof techniques. The proof assistant ensures the completeness and fault-freedom of the proofs. Theoretically, HOL is a general tool and capable of proving any mathematical theorem. Note that designing the proof strategy depends on expertise and user intervention, rather than complete automation. These tools have their own merits and shortcomings. Model checkers, such as SPIN and UPPAAL, offer more comprehensive modeling language and fully automatic verification process, thus is easier to use. However, the bottlenecks of model checkers are memory and expressiveness. If we use them on a large network, the state space is so huge that the memory can be rapidly ran out. Furthermore, their models can only express limited number of processes, thus the unbounded number of nodes are generally beyond their expressiveness. On the other hand, theorem provers, such as HOL, offer more powerful but more complex mathematical infrastructures for developing more general proofs. Therefore, as a shortcoming, they need more expertise and user intervention, thus cost more programmer-months. We believe that a better strategy is to combine the two types of tool. We may first verify a protocol using automated model checkers such as SPIN and UPPAAL, on some typical, fixed and small(-scale) networks. Although the proof is not complete, some faults will be discovered and then fixed. Once we ensure the correctness of the protocol on these small networks, we may use theorem provers such as HOL to generalize the result. For example, one instance of the strategy is to code a protocol first in SPIN and use HOL to address the limits of SPIN. This can be achieved by using HOL to prove the theorems on abstractions showing properties such as: if properties P 1 , ..., P n hold for small sets of (maybe abstracted) nodes S 1 , ..., S n , respectively, then property P will hold for arbitrarily many nodes. We use the abstraction proofs in HOL to reduce the memory demands of SPIN proofs, since each property P i is checked on a small enough (abstract) network S i . The abstraction proofs may also solve the problem of expressiveness. In fact, we largely reserve the comprehensibility and automation of model checking, but significantly reduce the memory demands of checking and increase the expressiveness of models by allowing user intervention in proving the theorems on abstractions. In essence, this strategy makes a tradeoff between memory consumption and the level of user intervention.