Formal verification of routing protocols for wireless ad hoc networks

Routing is one of the most basic and important tasks in a collaborative computer network. Having a correct, robust and efficient routing protocol is fun-damental to any wireless network. However, a difficult problem is how to guaran-tee these desirable qualities. Neither simulations nor testbed implementations can ensure the quality required for these protocols. As an alternative to these methods some researchers have successfully investigate the use of formal verification as a mean to guarantee the quality of routing protocols. Formal verification is a tech-nique that assures a system has, or has not, a given propriety, based on a formal specification of the system under evaluation. This technique has proved to be a valuable tool, even contradicting some authors' claims and informal proofs. This chapter presents the main tools, proposals and techniques available to perform formal verification of routing algorithms for wireless ad hoc networks.