Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-24559-6_26
Title: Towards a model checker for NesC and wireless sensor networks
Authors: Zheng, M.
Sun, J.
Liu, Y. 
Dong, J.S. 
Gu, Y.
Issue Date: 2011
Source: Zheng, M.,Sun, J.,Liu, Y.,Dong, J.S.,Gu, Y. (2011). Towards a model checker for NesC and wireless sensor networks. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6991 LNCS : 372-387. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-24559-6_26
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. © 2011 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/43175
ISBN: 9783642245589
ISSN: 03029743
DOI: 10.1007/978-3-642-24559-6_26
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

17
checked on Dec 13, 2017

Page view(s)

65
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.