Towards a model checker for NesC and wireless sensor networks
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 implement...
Saved in:
Main Authors: | , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2011
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/5030 https://ink.library.smu.edu.sg/context/sis_research/article/6033/viewcontent/Towards_a_Model.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-6033 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-60332020-03-12T08:39:04Z Towards a model checker for NesC and wireless sensor networks ZHENG, Manchun SUN, Jun LIU, Yang DONG, Jin Song GU, Yu 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-10-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5030 info:doi/10.1007/978-3-642-24559-6_26 https://ink.library.smu.edu.sg/context/sis_research/article/6033/viewcontent/Towards_a_Model.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Wireless Sensor Network Model Checker Operational Semantic Linear Temporal Logic State Reachability Programming Languages and Compilers Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Wireless Sensor Network Model Checker Operational Semantic Linear Temporal Logic State Reachability Programming Languages and Compilers Software Engineering |
spellingShingle |
Wireless Sensor Network Model Checker Operational Semantic Linear Temporal Logic State Reachability Programming Languages and Compilers Software Engineering ZHENG, Manchun SUN, Jun LIU, Yang DONG, Jin Song GU, Yu Towards a model checker for NesC and wireless sensor networks |
description |
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. |
format |
text |
author |
ZHENG, Manchun SUN, Jun LIU, Yang DONG, Jin Song GU, Yu |
author_facet |
ZHENG, Manchun SUN, Jun LIU, Yang DONG, Jin Song GU, Yu |
author_sort |
ZHENG, Manchun |
title |
Towards a model checker for NesC and wireless sensor networks |
title_short |
Towards a model checker for NesC and wireless sensor networks |
title_full |
Towards a model checker for NesC and wireless sensor networks |
title_fullStr |
Towards a model checker for NesC and wireless sensor networks |
title_full_unstemmed |
Towards a model checker for NesC and wireless sensor networks |
title_sort |
towards a model checker for nesc and wireless sensor networks |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2011 |
url |
https://ink.library.smu.edu.sg/sis_research/5030 https://ink.library.smu.edu.sg/context/sis_research/article/6033/viewcontent/Towards_a_Model.pdf |
_version_ |
1770575193938329600 |