A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks

TL;DR

This survey reviews formal verification techniques for ad hoc routing protocols in wireless sensor networks, comparing small-scale automatic methods and unbounded network abstractions for correctness proofs.

Contribution

It provides a comprehensive overview of existing formal verification approaches, highlighting their strengths, limitations, and how they complement each other in verifying routing protocol correctness.

Findings

Verification techniques can find faults and prove correctness.

Small-scale verification is automatic but limited in scope.

Unbounded network verification offers complete proofs but requires expertise.

Abstract

This paper surveys how formal verification can be used to prove the correctness of ad hoc routing protocols, which are fundamental infrastructure of wireless sensor networks. The existing techniques fall into two classes: verification on small-scale networks and verification on unbounded networks. The former one is always fully automatic and easy to use, thanks to the limited state space generated in verification. However, it cannot prove the correctness over all cases. The latter one can provide a complete proof based on abstractions of unbounded network. However, it usually needs user intervention and expertise in verification. The two kinds of technique are illustrated by verifications against some key properties such as stability, loop-freedom and deadlock-freedom. To conclude, they can be used to find faults and prove correctness, respectively. We believe that they can together aid the development of correct ad hoc routing protocols and their reliable implementations.