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

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

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.