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

CPS：协同：独立移动网络物理系统之间的协调行动

基本信息

批准号：
1646417
负责人：
Malte Jung
金额：
$ 80万
依托单位：
Cornell University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2016
资助国家：
美国
起止时间：
2016-09-01 至 2022-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1646417&HistoricalAwards=false
关键词：
CPS Synergy Coordinated Action Among

项目摘要

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.

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