CPS: Synergy: Coordinated Action Among Independent Mobile Cyber-Physical Systems

证明助手是一种编写可靠软件的编程技术，程序员不仅要编写程序代码，还要编写代码正确性的数学证明。然后，自动证明检查器要么验证代码是正确的，要么显示证明错误的地方，从而授权程序员修复不正确的假设。该项目侧重于自动驾驶汽车（AVs）的软件保障目标，自动驾驶汽车是复杂的网络物理系统，如多机器人团队，在世界上移动并相互交互。这些系统的例子包括自动驾驶汽车、用于检查和监视的自动无人机，以及用于灾难恢复的救援机器人。通过传感器和执行器与现实世界交互的程序必须对噪声传感器、物理、人类用户和程序无法控制的其他环境做出许多假设。智能的优点是三个工具来实现和证明复杂的自动驾驶汽车在嘈杂的现实世界中是正确的。这些工具使自动驾驶汽车能够处理日益复杂的交互。该项目将推动多种自动驾驶汽车和多cps系统软件保障的发展。该项目更广泛的意义和重要性在于，未来所有类型的自动驾驶汽车都必须能够在现实世界中安全部署，即使是在恶劣的条件下。各种自动驾驶系统的互操作性也将得到改善，这将有助于协调，例如在第一响应者之间。该项目将三个关键任务集成到网络物理系统的验证中，并发操作水平不断提高。首先，研究变压器在自动驾驶汽车上的应用。转换器是一种将复杂程序与相应简单程序的证明相结合的机制，以产生关于复杂程序的证明。这种方法将使工程师能够设计出能够在现实世界中安全、正确地相互交互的自动驾驶汽车，而无需手动证明处理传感和驱动错误的程序的多cps变体的正确性。在第二个任务中，该项目转向验证移动自动驾驶汽车的某些核心构建模块，包括快速探索随机树（RRT）运动规划器和卡尔曼滤波状态估计器。这项任务的核心挑战是证明使用连续统概率和其他实数（通常实现为浮点数）的算法的性质。由于浮点误差对验证存在障碍，pi转而利用建设性实数，它能够计算出任意精度的结果。在第三个任务中，该项目试图定义一个类型系统，作为对异构自动驾驶汽车的能力进行编码和执行推断的基础。这种能力的表示是灵活的、可扩展的，并且支持概率推理，从而考虑到感知和驱动错误。这项任务将实现密切的协调，即使是在从未遇到过彼此的自动驾驶汽车之间。

Proof assistants are a programming technique for writing trustworthy software, in which the programmer writes not only the program code but also a mathematical proof of the code's correctness. An automated proof checker then either verifies that the code is correct or shows where the proof is wrong, thus empowering the programmer to fix incorrect assumptions. This project focuses on the goal of software assurance for autonomous vehicles (AVs), which are complex cyber-physical systems, such as multi-robot teams, that move in the world and interact with one another. Examples of these systems include self-driving cars, automated drones for inspection and surveillance, and rescue robots for disaster recovery. Programs that interact with the real world through sensors and actuators must make many assumptions about noisy sensors, physics, human users, and other circumstances that cannot be controlled by the program. The intellectual merits are three tools to implement and prove complex AVs correct for noisy, real-world operations. These tools equip AVs to handle increasing levels of complexity of interaction. This project will lead to advances in software assurance of many kinds of AVs and multi-CPS systems. The project's broader significance and importance are that all kinds of AVs in the future must be built to be safe for real-world deployment, even under adverse conditions. Interoperability of diverse AV systems will also be improved, which will aid in coordination, for example among first-responders.The project integrates three key tasks into the verification of cyber-physical systems with increasing levels of concurrent operation. First, the project investigates the application of transformers to AVs. A transformer is a mechanism to combine a complex program with a proof about a corresponding simpler program in order to yield a proof about the complex program. This method will empower engineers to design AVs that can interact with one another safely and correctly in the real world without proving by hand the correctness of the multi-CPS variant of the program that handles errors in sensing and actuation. In the second task, the project turns to the verification of certain core building blocks of mobile AVs, including the rapidly-exploring random trees (RRT) motion planner and the Kalman filter state estimator. The core challenge in this task is to prove properties about algorithms that use continuum probabilities and other real numbers, typically implemented as floats. Since floating-point errors present an obstacle to verification, the PIs instead leverage constructive reals, which are capable of computing a result to arbitrary precision. In the third task, the project seeks to define a type system as the basis for codifying and performing inference about capabilities of heterogeneous AVs. This representation of capabilities is flexible, extensible, and supports probabilistic inference, thus accounting for sensing and actuation errors. This task will enable close coordination, even among AVs that have never encountered one another before.