Building Verifiable Sensing Applications Through Temporal Logic Specification

Sensing is at the core of virtually every DDDAS application. Sensing applications typically involve distributed communication and coordination over large self-organized networks of heterogeneous devices with severe resource constraints. As a consequence, developers must explicitly deal with low-level details, making programming time-consuming and error-prone. To reduce this burden, current sensor network programming languages espouse a model that relies on packaged reusable components to implement relevant pieces of a distributed communication infrastructure. Unfortunately, programmers are often forced to understand the mechanisms used by these implementations in order to optimize resource utilization and performance, and to ensure application requirements are met. To address these issues, we propose a novel and high-level programming model that directly exposes control over sensor network behavior using temporal logic specifications, in conjunction with a set of system state abstractions to specify, generate, and automatically validate resource and communication behavior for sensor network applications. TLA+ (the temporal logic of actions) is used as the underlying specification language to express global state abstractions as well as user invariants. We develop a synthesis engine that utilizes TLC (a temporal logic model-checker) to generate detailed actions so that user-provided behavioral properties can be satisfied, guaranteeing program correctness. The synthesis engine generates specifications in TLA+, which are compiled down to sensor node primitive actions. We illustrate our model using a detailed experimental evaluation on our structural sensing and control testbed. The proposed framework is integrated into the COSMOS macroprogramming environment, which is extensively used to develop sensing and control applications at the Bowen Lab for Structural Engineering at Purdue.