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.
Formal verification of routing protocols for wireless ad hoc networks
Book chapter N°8 in "Guide to wireless ad hoc networks", Springer, January 2009, ISBN: 978-1-84800-327-9
Systèmes de Communication
© Springer. Personal use of this material is permitted. The definitive version of this paper was published in Book chapter N°8 in "Guide to wireless ad hoc networks", Springer, January 2009, ISBN: 978-1-84800-327-9 and is available at : http://dx.doi.org/10.1007/978-1-84800-328-6_8
PERMALINK : https://www.eurecom.fr/publication/2657