.png){kind=icon}
返回
On software verification for sensor nodes
.png){kind=icon}
OA
AI
DOI：10.1016/j.jss.2011.04.054.png)
.png){kind=icon}
.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
We consider software written for networked, wireless sensor nodes, and specialize software verification techniques for standard C programs in order to locate programming errors in sensor applications before the software's deployment on motes. Ensuring the reliability of sensor applications is challenging: low-level, interrupt-driven code runs without memory protection in dynamic environments. The difficulties lie with (i) being able to automatically extract standard C models out of the particular flavours of embedded C used in sensor programming solutions, and (ii) decreasing the resulting program's state space to a degree that allows practical verification times. We contribute a platform-dependent, OS-independent software verification tool for OS-wide programs written in MSP430 embedded C with asynchronous hardware interrupts. Our tool automatically translates the program into standard C by modelling the MCU's memory map and direct memory access. To emulate the existence of hardware interrupts, calls to hardware interrupt handlers are added, and their occurrence is minimized with a double strategy: a partial-order reduction technique, and a supplementary reachability check to reduce overapproximation. This decreases the program's state space, while preserving program semantics. Safety specifications are written as C assertions embedded in the code. The resulting sequential program is then passed to CBMC, a bounded software verifier for sequential ANSI C. Besides standard errors (e.g., out-of-bounds arrays, null-pointer dereferences), this tool chain is able to verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals. Verification for wireless sensor network applications is an emerging field of research: thus, as a final note, we survey current research on the topic. (C) 2011 Elsevier Inc. All rights reserved.
Keyword:
Sensor
TelosB
MSP430
TinyOS
Verification
Bounded model checking
CBMC
AI总结
对已上传原文的论文进行重点信息的提取，主要内容包括：简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。
