Many deployments of Wireless Sensor Networks (WSNs) have failed due to software and hardware issues. Failures may hap- pen even after careful testing in simulation and testbeds, since the real-world conditions encountered at deployment time are in gen- eral different from those in the lab. These trigger untested execution paths, revealing previously unknown issues. As a result, assessing the correctness of WSN software is a major challenge.
The current practice includes using simulators/emulators to investigate the system behavior prior to deployment, or relying on WSN-speciﬁc debugging tools to deal with issues arising in the ﬁeld. Both types of solutions only identify issues when and if they arise.
In addition, the former approaches expose only a partial view on the possible system executions, dictated by arbitrary simulation parameters such as random seeds. The latter approaches, instead, may identify issues without however showing the corresponding causes. Some of these tools must also defend against so-called “heisenbugs”, where the debugging infrastructure affects the system behavior to the point of causing issues that would not be present otherwise.
Static veriﬁcation appears to be an ideal complement to the above approaches, providing complete and sound veriﬁcation of WSN software against user-speciﬁed properties. Completeness entails that a property violation is always found if present, whereas sound- ness guarantees that no false property violations are detected. The properties may describe desired behaviors or invariants over the system state, e.g., a requirement that a tree-based routing protocol never creates loops.
Upon detecting a property violation, the tools return counter-examples showing the complete system execution leading to the property violation. This represents an asset during development, as it makes easier to identify the causes of the issue. Existing approaches for static veriﬁcation of WSN software, however, focus on very speciﬁc problems, e.g., concurrency issues in multi-threading libraries.
Generalizing these solutions is difﬁcult because of the diversity in the functionality to verify. These range from application-level processing to hardware-speciﬁc functionality, and thus operate at different abstraction levels. In most cases, details that are relevant to an abstraction level are immaterial for others. Even within a single abstraction level, simple fragments of code may generate large state spaces.
Many of these states are generated only because of the generality of algorithms used in general-purpose tools, which do not exploit domain-speciﬁc knowledge to save on generated states. However, these states may not be necessary to examine for the property at hand.
Leveraging this observation we have develped Anquiro, a WSN-speciﬁc model checker. The tool works in a two-step fashion. The source code is ﬁrst translated into Anquiro-speciﬁc models. Next, it is veriﬁed against user-provided properties. Anquiro overcomes state space explosion problems during veriﬁcation by providing different abstraction levels depending on the functionality to verify.
For instance, if users want to verify the implementation of application-level functionality, the tool operates by abstracting away the low- level communication aspects that are irrelevant from the application perspective. These may include, for instance, different causes of packet losses, as the application is only interested in whether packets are lost, independently of the cause.
To demonstrate the use of Anquiro we report on its use in veriﬁcation of a widely used WSN dissemination protocol. As property to check, we study the core guarantee the protocol is to provide: the ability to eventually deliver data to all nodes. This shows us that the protocol may overlook an issue preventing correct operation.
We complete the discussion with an evaluation of Anquiro's run-time performance. Our results show that our domain-speciﬁc state abstractions provide orders of magnitude im- provements over standard approaches. This allows Anquiro to verify even large instances of our problem in reasonable time.
To read this external content in full, download the complete paper from the author's online archive.