Introduction

The concurrency, distributed execution, and real-time issues make sensor network applications especially vulnerable to software bugs. These bugs are transient in nature and are dependent on the timing of events, and hence are notoriously difficult to debug and catch. In this project, we focus on addressing the problem of developing provably reliable and robust software for sensor network applications.

Our approach is to first achieve correctness and fault-tolerance at the specification level and to preserve them via automatic code generation (refinement) while going to the implementation level. Since specifications are more succinct than implementations, our approach achieves scalability and simplicity in reasoning. Since we generate the implementation code from a verified specification automatically, our approach produces provably reliable and robust software.

We use the IOA language [1] for specification: IOA provides simple, abstract descriptions of distributed systems, invariants, and simulation relations. We use the IOA toolkit for verification at the specification level and subsequently to refinement of the verified system to the implementation level: The IOA Toolkit provides a set of tools that support the rigorous specification, analysis, and generation of distributed systems. At the implementation level, we target the TinyOS [2] platform. TinyOS, developed by UC Berkeley, is a popular operating system for wireless sensor networks. It features a component-based architecture and is very suitable for modeling in IOA.

To summarize, our goals are:

1. Facilitating the verification of distributed sensor network applications,
2. Providing provably reliable implementations via automatic code generation, and
3. Making sensor network programming accessible to non specialists.

Approach

Our earlier experimentation on TinyOS found that TinyOS is very suitable for IOA modeling. TinyOS features a component-based architecture; the component library includes network protocols and sensor drivers accompanied with interfaces. An interface declares a set of functions called commands that the interface provider must implement and another set of functions called events that the interface user must implement. An application consists of (1) components written by the application designer and (2) the library components that are used by the components in (1). These components are linked together by ``wiring'' their interfaces to form an executable. When modeling these components, the interfaces correspond to labels for input output signals. This way, for a component C, commands from all components that use C and events from all components that C uses correspond to the input transitions of C. Similarly, the commands from C to the components C uses, and the events that C raises correspond to output transitions of C.

Our proposed method for TinyOS code generation takes as input an IOA/TIOA specification of the target application. Our earlier experiments found that TinyOS applications are very suitable for IOA/TIOA modeling. TinyOS features a component-based architecture; the component library includes network protocols and sensor drivers accompanied with interfaces. An application consists of an application component written by the application developer and the library components that are used by that application component. These components are linked together by ``wiring'' their interfaces to form an executable. When modeling these components in IOA, a component correspond to an automaton and its associated interfaces correspond to labels for input output signals of the automaton.

More specifically, our proposed method involves the following tasks.

1. Coding key components of TinyOS library in IOA/TIOA: since these library components are reused by several applications, and since our compositional approach offers reusability, this one-time modeling will expedite the user's job significantly,
2. Compiler development for achieving compilation from IOA/TIOA to TinyOS: to this end we will leverage on previous work on code generation from IOA models [3], and
3. Proving the correctness of the compiler: this one-time proof will ensure that the compiled programs preserve the properties of the abstract IOA/TIOA programs.

For generating verified TinyOS code, the user of our tool will perform only the following three steps.

1. Coding the application component using the IOA/TIOA language: since the TinyOS library components are already coded using IOA, the user needs to code only the application component,
2. Verifying the correctness of the composed distributed system using the IOA toolkit: the IOA toolkit [1] instantiates user's code on multiple nodes, and provides support for rigorous verification of this composed distributed application, and
3. Compiling the application component to get the corresponding TinyOS code: since the composed distributed system is proved correct at the abstract level, the resultant system at the TinyOS level will also be correct. Joshua Tauber's thesis [3], that presented an IOA to Java code generator, is closely related for this process.

Status

We have made progress in task 1, coding key components of TinyOS library in IOA. We coded the Surge application included in TinyOS distribution as a case study. In the Surge application, each node takes light sensor readings and forwards them to a base station. To this end, Surge uses the MultiHopRouter module (consisting of MultiHopEngineM and MultiHopLEPSM components), a shortest-path routing algorithm with a single destination node (base station). After coding the MultiHopEngineM and MultiHopLEPSM components in IOA, we are working on extending the MultiHopRouter module to be able to route messages to any destination and not just to a single root. We are also investigating ways to tune the MultiHopRouter module to get acceptable robustness and performance.

Next, we will perform a hand translation of our modified MultiHopRouter module back to TinyOS level code. After this case study, we will work on task 2, the IOA to TinyOS compiler development.

Research Support

This project is supported by DARPA Air Force contract number FA9550-04-C-0084, DARPA Award number F33615-01-C-1896, NSF Award numbers CCR-0326277 and CCR-0121277, NSF-Texas Engineering Experiment Station grant 64961-CS, DARPA/AFOSR MURI Award F49620-02-1-0325 and MURI AFOSR Award Number SA2796PO 1-0000243658.

References:

[1] Stephen Garland, Nancy Lynch, Joshua Tauber, and Mandana Vaziri. IOA User Guide and Reference Manual. Technical Report MIT-LCS-TR-961, MIT Computer Science and Artificial Intelligence Laboratory (CSAIL), Cambridge, MA, 2004.

[2] J. Hill, R. Szewczyk, A. Woo, S. Hollar, D. Culler, and K. Pister. System architecture directions for network sensors. ASPLOS, pp. 93--104, 2000.

[3] Joshua A. Tauber. Verifiable Compilation of I/O Automata without Global Synchronization. Massachusetts Institute of Technology, Cambridge, MA, Sept 2004.