Achieving dependability in sensor networks through automated requirements-based programming

A sensor network can be viewed as a distributed system consisting of many nodes (processes) that communicate and exchange data. Such a system, including an application running on top of the sensor network, is inherently difficult to model and validate. System requirements and actual application code may not be consistent, with the implementation failing to implement all of the requirements, or failing to implement them correctly. Requirements can be expressed as a set of services that the sensor network should provide. Each service may be described using one or more scenarios. For the classes of systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or in other appropriate notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations. This represents a significant step forward toward high-dependability system engineering for numerous possible application domains, including sensor networks.