CPS: Breakthrough: Rigorous Integration of Decision Procedures and Numerical Algorithms for the Formal Verification of Cyber-Physical Systems

CPS：突破：决策程序和数值算法的严格集成，用于网络物理系统的形式验证

• 批准号: 1330014
• 负责人: Frank Pfenning
• 金额: $ 49.97万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-10-01 至 2018-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1330014&HistoricalAwards=false
• 关键词: CPS; Breakthrough; Rigorous; Integration; Decision

This project establishes a new framework for the formal verification of cyber-physical systems. The framework combines the power of logical decision engines and scalable numerical methods to perform safety verification of general nonlinear hybrid systems. The key difficulty with formal verification of hybrid systems is that all scalable modern verification techniques rely heavily on the use of powerful decision procedures. For hybrid systems, one needs to reason about logic formulas over the real numbers with nonlinear functions, which has been regarded as an intractable problem. The project proposes new directions for tackling the core decision problems, with the combined power of logical and numerical algorithms. The research directly leads to the development of practical tools that will push the frontier of verification of realistic cyber-physical systems to a brand new level.This project aims at fundamental research of problems that stand at the core of the design, analysis, and implementation of reliable cyber-physical systems. It combines techniques from logic, numerical analysis, and automated reasoning, and will produce a unifying methodology that is powerful to address main challenges in this field. The techniques developed in this project will significantly enhance the complexity and reliability of the next generations of cyber-physical systems. Cyber-physical systems are ubiquitous in safety-critical applications as diverse as aerospace, automotive, civil infrastructure, energy, manufacturing, and healthcare. Malfunctioning cyber-physical systems can have catastrophic economic and societal consequences. This project will have a broad range of impact in these areas. This research aims to significantly enhance the management of complexity and reliability of the next generations of cyber-physical systems, and will broadly impact all the application areas.

该项目为正式验证网络物理系统建立了一个新的框架。该框架结合了逻辑决策引擎的力量和可扩展的数值方法，以执行一般非线性混合系统的安全验证。正式验证混合系统的关键困难在于，所有可扩展的现代验证技术都在很大程度上取决于强大的决策程序的使用。对于混合系统，需要对具有非线性功能的实际数字上的逻辑公式进行推理，这被认为是一个棘手的问题。该项目通过逻辑和数值算法的综合力量提出了解决核心决策问题的新指示。这项研究直接导致开发实用工具，这些工具将将现实的网络物理系统的验证前端推向一个全新的水平。该项目旨在基本研究对可靠的网络物理系统的设计，分析和实施的核心问题。它结合了逻辑，数值分析和自动推理的技术，并将产生一种统一的方法，该方法可以强大，以应对该领域的主要挑战。该项目中开发的技术将显着提高下一代网络物理系统的复杂性和可靠性。网络物理系统在安全性关键应用中无处不在，例如航空航天，汽车，民用基础设施，能源，制造业和医疗保健。网络物理系统故障可能会带来灾难性的经济和社会后果。该项目将在这些领域产生广泛的影响。这项研究旨在显着增强下一代网络物理系统的复杂性和可靠性的管理，并将广泛影响所有应用领域。