SHF: Small: Practical and Formal Foundations for Intermittent Computer Systems

间歇性、能量收集、无电池设备是廉价、小型和低维护的设备，用于构建计算、传感和通信系统，这些系统将成为未来物联网、边缘计算和传感以及网络物理系统的基础。 然而，间歇性的软件执行可能会使设备变得不可靠，因为设备的电源故障和充电周期难以预测，从而使部署到高保证应用程序变得复杂。该项目定义了第一个正式的模型，以精确地描述间歇性系统的行为，形式化所需的正确性属性，设计和实现新的复杂的间歇性系统是正确的，并构建代表间歇性系统的实际应用的基准。 该项目的影响在于其技术发展使间歇性系统能够执行复杂任务，同时更安全可靠，从而允许更广泛地部署到网络物理和物联网应用中。该项目的关键技术贡献在于其间歇性计算的正式模型，从顺序模型开始，然后扩展到在存在具有定时要求的外围设备的情况下的并发操作。 这些模型精确地描述了系统行为，允许对部署的系统进行正确性证明。适应这些模型的调度，该项目开发了第一个可证明正确的能量收集和计算调度器的间歇性系统。 该项目建立了规则，用于验证一组计算任务相对于能量约束的可行性，并允许优雅的退化时，没有时间表是可行的。 该项目产生的基准汇总并全面表征了独立开发的应用程序，从而实现了系统之间的直接比较。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Intermittent, energy-harvesting, battery-less devices are cheap, small, and low-maintenance devices for building computing, sensing, and communicating systems that will serve as the foundation for future internet of things, edge computing and sensing, and cyber physical systems. However, intermittent software execution can make a device unreliable, due to the device's hard-to-predict power failure and recharge cycles, complicating deployment to high-assurance applications. This project defines the first formal models to precisely characterize the behavior of intermittent systems, formalizes desired correctness properties, designs and implements new sophisticated intermittent systems that are correct, and constructs benchmarks representative of real-world applications of intermittent systems. This project's impacts are that its technical developments make intermittent systems capable of complex tasks, and at the same time, safer and more reliable, thereby allowing wider deployment into cyber-physical and internet-of-things applications.The key technical contributions of this project are in its formal models of intermittent computing, starting with a sequential model, then extending to concurrent operations in the presence of peripheral devices with timing requirements. These models characterize system behavior precisely, allowing for correctness proofs of deployed systems. Adapting these models to scheduling, this project develops the first provably correct energy collection and computation scheduler for intermittent systems. The project establishes rules for verifying feasibility of a set of computing tasks with respect to energy constraints, and allows for graceful degradation when no schedule is feasible. Benchmarks produced by this project aggregate and thoroughly characterize independently developed applications, enabling direct comparison between systems.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.