Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

10-2011

Abstract

Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled as the composition of sensors with a network topology. Verifications of individual sensors and the whole WSN become possible by exploring the corresponding LTSs using model checking. With substantial engineering efforts, we implemented this approach in the tool NesC@PAT to support verifications of deadlock-freeness, state reachability and temporal properties for WSNs. NesC@PAT has been applied to analyze and verify WSNs, with unknown bugs being detected. To the best of our knowledge, NesC@PAT is the first model checker which takes NesC language as the modeling language and completely preserves the interrupt-driven feature of the TinyOS execution model.

Keywords

Wireless Sensor Network, Model Checker, Operational Semantic, Linear Temporal Logic, State Reachability

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28

First Page

372

Last Page

387

ISBN

9783642245589

Identifier

10.1007/978-3-642-24559-6_26

Publisher

Springer Link

City or Country

Durham, UK

Additional URL

https://doi.org/10.1007/978-3-642-24559-6_26

Download

Share

COinS