Improving TinyOS Developer Productivity with Statecharts

Volker Menrad, Miguel Garcia, Sibylle Schupp

Abstract 

The development of sensor network software is challenging due to 
(a) the emergence at runtime of nonintuitive component interactions; and 
(b) the difficulty of debugging non-reproducible bugs, especially those arising from 
timing and scheduling conditions. These features are inherent to the TinyOS programming model 
(which involves wiring off-the-shelf and custom components, to communicate over interfaces) and thus 
approaches are needed to increase both productivity and quality measures of sensornet development. 
The state of the practice involves documenting interface contracts in natural language, 
so as to write components that fulfill the expectations of the invoked component (its preconditions), 
upon which a guarantee is obtained about the resulting component state (its postconditions). 
Experience has shown that this kind of technical documentation leaves room for misunderstanding, and thus 
a more precise format is required to capture these contracts. Using real-world examples we show how 
a rich statechart language 
(a) can be used to achieve readable yet more precise formulations of interface contracts; 
(b) in the future can also serve as a basis for automated verification of nesC code (i.e., 
to determine whether such code abides by the contracts formalized with statecharts). 
Our case studies build upon previous work on contract specification for component-based software, 
however to our knowledge this is the first time that an expressive statechart language is systematically used 
to capture full-fledged TinyOS behavioral contracts, with an eye towards the compile-time verification of contracts.