FMitF: Track I: Robust Enforcement of Customizable Resource Constraints in Heterogeneous Embedded Systems

Heterogeneous embedded systems are becoming more pervasive and more complex. These systems often feature resource-constrained architectures consisting of different types of processing units connected to a variety of sensors and actuators that interact with the physical world. Here, correctness depends on the physical requirements associated with performing those computations.

For example, inefficient computations that exhaust the available energy on a battery-powered done can result in a system-level failure. A major shortcoming of previous work is that analytical correlations between physical actuators and computational hardware/software parameters were developed on a per application/domain basis, which limits generality.

This project focuses on enabling embedded-systems development with respect to customizable constraints on system-wide resource usage (time, energy, etc.). It will utilize formal methods to develop a unified approach that addresses issues arising due to the trade-offs between computation, actuation, and sensing. The framework developed in this project seeks to improve the embedded-systems design process by increasing both the level of automation and the level of confidence in system correctness.

The goal of the proposed improvements to reliability, computational hardware needs, and rapid prototyping is to reduce costs and increase deployment of embedded systems, particularly in resource-constrained scenarios.

The core technical contributions are: (I) a novel analytical modeling approach to characterize resource inter-dependencies on heterogeneous embedded architectures; (II) formal techniques to analyze software control programs which violate given resource constraints, and automatically repair such programs to ensure adherence to the constraints; and (III) a flexible dynamic approach for dealing with situations where the environment deviates from the system designer's assumptions. Specific techniques explored in the work will be (1) a flexible analytical model used to describe how interactions between computation, actuation, and sensing influence resource usage in embedded heterogeneous systems; (2) a specification language for customizable resource constraints, which enables complex reasoning about system resource usage, along with functionality to generate efficient approximations at granularities driven by the specification; (3) a program repair engine that uses syntax-guided synthesis to automatically ensure that the control software keeps the embedded system within the resource constraints; (4) techniques for coupling synthesis with task-motion planning to increase the usability of repair; and (5) a technique for quickly synthesizing and compactly representing alternative control programs, that will enable fast-failover of the embedded system in cases where the environment deviates from expectations.

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.