Enabling efficient static verification of sensor network software - Embedded.com

Enabling efficient static verification of sensor network software

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-specific debugging tools to deal with issues arising in the field. 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 verification appears to be an ideal complement to the above approaches, providing complete and sound verification of WSN software against user-specified 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 verification of WSN software, however, focus on very specific problems, e.g., concurrency issues in multi-threading libraries.

Generalizing these solutions is difficult because of the diversity in the functionality to verify. These range from application-level processing to hardware-specific 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-specific 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-specific model checker. The tool works in a two-step fashion. The source code is first translated into Anquiro-specific models. Next, it is verified against user-provided properties. Anquiro overcomes state space explosion problems during verification 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 verification 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-specific 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. 

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.