.png){kind=icon}
.png){kind=icon}
Return
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}
Share.png){kind=icon}
Save
Abstract
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.
Keywords:
Sensor
TelosB
MSP430
TinyOS
Verification
Bounded model checking
CBMC
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
4.1
Papers:
5.4K
Citations:
8.4K