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

点击翻译按钮获取中文摘要

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.