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.

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