权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

CPS: Small: Sound Invariant Generation for Continuous and Hybrid Systems

CPS：小型：连续和混合系统的声音不变生成

基本信息

批准号：
1739629
负责人：
Andre Platzer
金额：
$ 47.91万
依托单位：
Carnegie-Mellon University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2017
资助国家：
美国
起止时间：
2017-09-01 至 2022-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1739629&HistoricalAwards=false
关键词：
CPS Small Sound Invariant Generation

项目摘要

This project considers the pragmatic challenge of broadening the reach and general accessibility of cyber-physical system (CPS) analysis. It capitalizes on logical foundations for cyber-physical systems to study automated analysis for CPS without sacrificing correctness of the analysis results. While the complexities of CPSs can be quite demanding, there is a considerable pragmatic difference between rigorous reasoning techniques that are available to verification experts compared to techniques that provide a vast amount of automation support to become more accessible for novices and more productive for experts. This project focuses on finding invariants, which convey crucial insights about quantities or relationships, such as minimum safety distances, that do not change while the CPS drives or flies.Cyber-physical systems such as self-driving cars, advanced computerized car safety technology, and drones have considerable potential to change the world for the better. Their designs face intensive safety requirements, however, and feature increasingly complex behaviors. The advanced but correct automation of CPS analysis technology developed in this project is crucial to broaden the reach of trustworthy verification and validation results. In the long run, there is a chance that this technology will fundamentally change the way that CPS are engineered by enabling CPS engineers to have increasingly comprehensive safety analysis tools at their fingertips. As a demonstration with considerable impact potential, this project studies safe control functionalities for quadrotors. Quadcopters are a popular choice for realizing many applications, but their safety is a nontrivial challenge. Not every company or grass-roots effort will have the capacity to conduct a full verification and validation effort. That is why a set of baseline functionalities that have been preverified are expected to be a helpful basis for such designs. The results of this project, including CPS models, controllers, proofs, and tools, will be made available on the KeYmaera X web page: http://keymaeraX.org/

该项目考虑了扩大网络物理系统（CPS）分析的范围和一般可访问性的务实挑战。它利用网络物理系统的逻辑基础来研究 CPS 的自动化分析，而不牺牲分析结果的正确性。虽然 CPS 的复杂性可能相当高，但验证专家可用的严格推理技术与提供大量自动化支持的技术之间存在相当大的实用差异，这些技术对于新手来说更容易使用，对于专家来说更高效。该项目的重点是寻找不变量，这些不变量传达了关于数量或关系的重要见解，例如最小安全距离，这些数量或关系在 CPS 驾驶或飞行时不会改变。自动驾驶汽车、先进的计算机化汽车安全技术和无人机等网络物理系统具有巨大的潜力，可以让世界变得更美好。然而，他们的设计面临着严格的安全要求，并且具有日益复杂的行为。该项目中开发的先进而正确的 CPS 分析技术自动化对于扩大可信验证和确认结果的范围至关重要。从长远来看，这项技术有可能从根本上改变 CPS 的设计方式，让 CPS 工程师能够轻松掌握日益全面的安全分析工具。作为具有相当大影响潜力的演示，该项目研究四旋翼飞行器的安全控制功能。四轴飞行器是实现许多应用的流行选择，但其安全性是一个不小的挑战。并非每个公司或基层工作都有能力进行全面的验证和确认工作。这就是为什么一组已经预先验证的基线功能有望成为此类设计的有用基础。该项目的结果，包括 CPS 模型、控制器、证明和工具，将在 KeYmaera X 网页上提供：http://keymaeraX.org/

项目成果

期刊论文数量（9）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Learning to find proofs and theorems by learning to refine search strategies

通过学习改进搜索策略来学习找到证明和定理

DOI：
发表时间：
2022
期刊：
Advances in neural information processing systems
影响因子：
0
作者：
Laurent, Jonathan;Platzer, André
通讯作者：
Platzer, André

Implicit Definitions with Differential Equations for KeYmaera X (System Description)

DOI：
10.1007/978-3-031-10769-6_42
发表时间：
2022-03
期刊：
ArXiv
影响因子：
0
作者：
James Gallicchio;Yong Kiam Tan;Stefan Mitsch;André Platzer
通讯作者：
James Gallicchio;Yong Kiam Tan;Stefan Mitsch;André Platzer

A verified decision procedure for univariate real arithmetic with the BKR algorithm.

使用 BKR 算法验证单变量实数算术的决策过程。

DOI：
发表时间：
2021
期刊：
12th International Conference on Interactive Theorem Proving (ITP 2021
影响因子：
0
作者：
Cordwell, Katherine;Tan, Yong Kiam;Platzer, André
通讯作者：
Platzer, André

A Formal Safety Net for Waypoint-Following in Ground Robots

地面机器人航路点跟踪的正式安全网

DOI：
10.1109/lra.2019.2923099
发表时间：
2019
期刊：
IEEE Robotics and Automation Letters
影响因子：
5.2
作者：
Bohrer, Brandon;Tan, Yong Kiam;Mitsch, Stefan;Sogokon, Andrew;Platzer, Andre
通讯作者：
Platzer, Andre

Verified quadratic virtual substitution for real arithmetic

经验证的实数算术的二次虚拟替代