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

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

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.