Deriving State Machines from TinyOS Programs Using Symbolic Execution

The most common programming languages and platforms for sensor networks foster a low-level programming style. This design provides fine-grained control over the underlying sensor devices, which is critical given their severe resource constraints. However, this design also makes programs difficult to understand, maintain, and debug. In this paper, we describe an approach to automatically recover the high-level system logic from such low-level programs, along with an instantiation of the approach for nesC programs running on top of the TinyOS operating system. We adapt the technique of symbolic execution from the program analysis community to handle the event-driven nature of TinyOS, providing a generic component for approximating the behavior of a sensor network application or system component. We then employ a form of predicate abstraction on the resulting information to automatically produce a finite state machine representation of the component. We have used our tool, called FSMGen, to automatically produce compact and fairly accurate state machines for several TinyOS applications and protocols. We illustrate how this high-level program representation can be used to aid programmer understanding, error detection, and program validation.