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

异构嵌入式系统正变得越来越普遍和复杂。这些系统通常具有资源受限的架构，由不同类型的处理单元组成，这些处理单元连接到与物理世界交互的各种传感器和执行器。在这里，正确性取决于与执行这些计算相关的物理需求。例如，低效的计算会耗尽电池供电的计算机上的可用能量，从而导致系统级故障。以前工作的一个主要缺点是物理执行器和计算硬件/软件参数之间的分析相关性是在每个应用/领域的基础上开发的，这限制了通用性。这个项目关注于在系统范围内的资源使用（时间、能量等）的可定制约束下实现嵌入式系统开发。它将利用正式的方法来开发一种统一的方法来解决由于计算、驱动和传感之间的权衡而产生的问题。本项目开发的框架旨在通过提高自动化水平和对系统正确性的信心水平来改进嵌入式系统设计过程。建议改进可靠性、计算硬件需求和快速原型的目标是降低成本并增加嵌入式系统的部署，特别是在资源受限的场景中。核心技术贡献有：(1)一种新的分析建模方法来表征异构嵌入式架构上的资源相互依赖性；（II）分析违反给定资源约束的软件控制程序，并自动修复这些程序以确保遵守约束的正式技术；（III）灵活的动态方法，用于处理环境偏离系统设计者假设的情况。在工作中探索的具体技术将是：(1)一个灵活的分析模型，用于描述计算、驱动和感知之间的交互如何影响嵌入式异构系统中的资源使用；(2)可定制资源约束的规范语言，它支持对系统资源使用情况的复杂推理，以及由规范驱动的在粒度上生成有效近似的功能；(3)程序修复引擎，该引擎使用语法引导合成自动确保控制软件将嵌入式系统保持在资源约束范围内；(4)结合任务运动规划的耦合综合技术，提高维修的可用性；(5)一种快速合成和紧凑表示可选控制程序的技术，这将在环境偏离预期的情况下实现嵌入式系统的快速故障转移。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.