FMitF: Track I: Probabilistic Modeling and Analysis Tools for Intermittent Systems

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

The goal of this project is to drastically simplify software development for intermittent systems by creating practical tools for modeling and analyzing the energy management and timing of intermittent software. Intermittent systems operate without a battery or tethered power supply and instead harvest energy from their environment, using motion, temperature gradients, and light. Eliminating the reliance on batteries improves robustness and reduces maintenance requirements, making intermittent systems suitable for deployment in harsh environments such as space or inside the body. Managing the interaction of energy collection and storage, intermittent operation, and the consequences of power failures are key challenges for the design of intermittent software. The project’s novelties are to address these challenges by using novel probabilistic modeling and analysis techniques to create serviceable timing and energy models for intermittent systems together with diagnosis tools that provide feedback during software development. The project's impacts are that energy and timing failures in intermittent systems can be diagnosed at development time and avoided without time-consuming trial-and-error experiments that run software on the target device. Moreover, the theoretical foundations of probabilistic programming for energy use in this domain enable a system designer to express, reason about, and validate energy consumption of mission critical embedded systems in domains like chip-scale satellites and in-body medical devices. The main technical innovation of the proposed work is to develop probabilistic programming as a tool for modeling and formally analyzing the energy use and execution time of intermittent systems. Probabilistic programming is an emerging technology that provides an efficient and flexible interface for Bayesian machine learning. Advantages of Bayesian learning include robustness and the ability to quantify uncertainty. For intermittent systems, probabilistic programs can serve as the link between a static analysis that is sound with respect to the formal semantics of probabilistic programs and a measurement-based energy model that can incorporate detailed domain knowledge about the hardware. The project focuses on the most challenging aspects of this approach and builds on the preliminary results and complementary strengths of the investigators in probabilistic programming, static analysis of probabilistic programs, intermittent systems, and the design and implementation of intermittent software. The main objectives are (1) developing and experimentally validating an effective methodology for creating probabilistic energy and timing models of different complexity and at different abstraction levels, (2) designing static analyses that automatically derive tail bounds on the computational costs as described by the models and to apply these bounds to provide global timing guarantees and (3) to apply and test the methodology in a cooperative scheduler and runtime system that uses probabilistic energy predictions to ensure fairness of energy consumption across tasks in an intermittent execution. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.