Supporting the Specification and Runtime Validation of Asynchronous Calling Patterns in Reactive Systems

Wireless sensor networks (“sensornets”) are highly distributed and concurrent, with program actions bound to external stimuli. They exemplify a system class known as reactive systems, which comprise execution units that have “hidden” layers of control flow. A key obstacle in enabling reactive system developers to rigorously validate their implementations has been the absence of precise software component specifications and tools to assist in leveraging those specifications at runtime. We address this obstacle in three ways: (i) We describe a specification approach tailored for reactive environments and demonstrate its application in the context of sensornets. (ii) We describe the design and implementation of extensions to the popular nesC tool-chain that enable the expression of these specifications and automate the generation of runtime monitors that signal violations, if any. (iii) Finally, we apply the specification approach to a significant collection of the most commonly used software components in the TinyOS distribution and analyze the overhead involved in monitoring their correctness