CPS:Small: Syntax-Guided Synthesis for Cyber-Physical Systems

如今，任何人都可以购买并组装传感器、执行器和计算组件，但通常只有训练有素的工程师才能组成能够自主执行复杂任务的系统。该项目通过创建计算工具，使人们能够选择一组构建模块并定义系统应该做什么，从而使任何人都可以访问网络物理系统（CPS）的设计。然后，这些工具自动创建一个简单且易于理解的描述，说明如何组装组件并提供完成任务所需的控制。如果任务不能用单个系统完成，则工具提供需要组装的多个系统和/或解释为什么不能完成任务，例如由于物理限制。该项目包括设计一个竞赛，以加速设计工具的开发，并指导来自代表性不足群体的学生。受程序综合、控制综合和模块化CPS进步的启发，该项目(i)定义了任务需要在物理环境中运动的CPS的正式规范和综合过程，（ii）创建了综合CPS的结构和控制的自动化设计工具，并保证完全或部分满足任务。形式化和工具是基于语法引导的综合（SyGuS）范式，其中设计空间通过考虑额外的结构和利用计算方法从可满足性模块理论（SMT）求解器到程序综合工具，逆运动学求解器，运动规划器和设计优化来减少。这些工具在两个物理平台和两个模拟平台上进行了评估。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Nowadays, anyone can buy and put together sensors, actuators, and computation components, but typically only highly trained engineers are able to compose systems that can autonomously perform complex tasks. This project makes the design of cyber-physical systems (CPS) accessible to anyone by creating computational tools that enable people to choose a set of building blocks and define what a system should do. The tools then automatically create a simple and easy to understand description of how to assemble the components and provide the control needed to accomplish the task. If the task cannot be done with a single system, the tools provide either multiple systems that need to be assembled and/or explanations as to why the task cannot be done, for example due to physical constraints. The project includes designing a competition to accelerate the development of design tools, and mentoring of students from underrepresented groups. Inspired by advances in program synthesis, control synthesis and modular CPS, this project (i) defines formal specifications and synthesis processes for CPS whose task requires motion in the physical environment, and (ii) creates automated design tools that synthesize both the structure and control of the CPS and that guarantee either full or partial task satisfaction. The formalisms and tools are based on the Syntax-Guided Synthesis (SyGuS) paradigm where the design space is reduced by considering additional structure and leverages computational methods from satisfiability-modulo-theories (SMT) solvers to program synthesis tools, inverse kinematics solvers, motion planners and design optimization. The tools are evaluated on two physical and two simulated platforms.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.