Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

1-2013

Abstract

Wireless sensor networks may be used to conduct critical tasks like fire detection or surveillance monitoring. It is thus important to guarantee the correctness of such systems by systematically analyzing their behaviors. Formal verification of wireless sensor networks is an extremely challenging task as the state space of sensor networks is huge, e.g., due to interleaving of sensors and intra-sensor interrupts. In this work, we develop a method to reduce the state space significantly so that state space exploration methods can be applied to a much smaller state space without missing a counterexample. Our method explores the nature of networked NesC programs and uses a novel two-level partial order reduction approach to reduce interleaving among sensors and intra-sensor interrupts. We define systematic rules for identifying dependence at sensor and network levels so that partial order reduction can be applied effectively. We have proved the soundness of the proposed reduction technique, and present experimental results to demonstrate the effectiveness of our approach.

Keywords

Sensor Network, Wireless Sensor Network, Model Chec, Linear Temporal Logic, Task Sequence

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, Rome, Italy, January 20-22

First Page

515

Last Page

535

ISBN

9783642358722

Identifier

10.1007/978-3-642-35873-9_30

Publisher

Springer Link

City or Country

Rome, Italy

Additional URL

https://doi.org/10.1007/978-3-642-35873-9_30

Download

Share

COinS