Runtime Verification for Wireless Sensor Network Applications

Abstract

We present a case study that considers the application of runtime verification technology to a wireless sensor application.  The case study is performed using the SURGE TinyOS application for multi-hop routing, which executes on the Avrora TinyOS simulator.  We discuss the problems we have encountered in the course of case study.  The problems include unclear correctness properties for wireless network applications (indicating ad hoc development process) and inadequate tool support.

A wireless sensor network usually comprises of a collection of tiny
devices with built-in processors that can gather physical and
environment information such as temperature, light, sound, etc., and
communicate with one another over radio.  Many wireless sensor network
applications sit on top of an operating system called TinyOS and 
are mostly written in nesC, an extension of C that provides a component-based
programming paradigm.  Most of wireless sensor network applications
are developed and tested on a simulator before they are deployed in
the environment because testing and debugging directly on physical
devices are very difficult, especially when the network consists of
many nodes, and may not provide enough information for debugging.  A
simulator usually produces detailed execution information and can help
find errors.  However, even with the simulator and nesC, the
current state of development tools for wireless sensor network still
requires very low-level programming, which makes it hard for the
developers to maintain a high-level view of the system operation.
During the validation stage, lack of sophisticated debugging tools for
sensor networks makes it difficult to make the connection between a
high-level functional or performance requirement and a particular
aspect of system implementation.

This paper investigates a high-level approach to examine execution
data from a simulator and analyze it using runtime verification.  The
technique 1) identifies and formally specifies high-level requirements
for the system under development, 2) monitors a distributed wireless
sensor network application using data provided by the simulator, and 3)
checks for timing and dynamic properties to gain understanding of the
relevant behaviors of wireless sensor nodes and to provide a
systematic approach in finding bugs and errors.  A particular runtime verification 
used inthis paper is MaC.  MaC provides specification
languages capable of expressing functional, timing, and probabilistic
properties to specify requirements or patterns of errors.  Properties
can, for example, examine periodic behaviors or identify a faulty node.
MaC then monitors and checks a wireless sensor network application
against its specification by observing data produced by a simulator.

The motivation for applying the monitoring and checking technique
to check wireless sensor network applications is threefold: 1)
raise the development level for wireless sensor network, 2)
provide a mechanism for understanding high-level behaviors of the
system in terms of low-level observation, and 3) provide a tool
based on the acceptance of the state of the art development tool for
sensor networks.