CAREER: Automatic Analysis of Cyber Physical Systems: Bridging the Gap between Research and Industrial Practice

该项目的目标是开发复杂的正式验证工具，以发现网络物理系统中的有害缺陷。网络物理系统负责安全关键系统中的许多控制任务，例如汽车，航空电子设备，医疗设备和配电系统。保证这些系统的正确性至关重要。 然而，现有的验证和确认技术已经远远低于解决这一重要的challenge.This项目研究验证技术分析大型和复杂的网络物理系统。 首先，该项目正在开发丰富的建模形式主义，能够在正确的抽象级别上捕获现实的系统设计。 这些形式主义形成了验证技术的基础，可用于查明网络物理系统中的功能缺陷。 具体来说，该项目的重点是检测有害的数值精度损失的控制系统中使用固定和浮点数实现的技术。 最后，该项目解决了使用区间分析，凸优化和符号决策程序验证复杂非线性系统的挑战。 这项研究的结果以开源工具的形式提供给社区。这些工具将直接支持复杂系统的验证。该项目的教育影响在于将研究与以严格的网络物理系统软件工程为主题的课程整合。由此产生的课程提供了宝贵的培训，本科生以及研究生在使用先进的验证工具和技术，以确保系统的安全和可靠的设计。

The goal of this project is to develop sophisticated formal verification tools for finding harmful defects in cyber-physical systems. Cyber-physical systems are responsible for numerous control tasks in safety-critical systems such as automobiles, avionics, medical devices, and power distribution systems. Guaranteeing the correctness of these systems is of the utmost importance. However, existing verification and validation techniques have fallen far short of addressing this important challenge.This project investigates verification techniques for analyzing large and complex cyber-physical systems. First, the project is developing rich modeling formalisms that are capable of capturing realistic system designs at the right levels of abstraction. These formalisms form the basis for verification techniques that can be used to pinpoint functional defects in cyber-physical systems. Specifically, the project focuses on techniques for detecting harmful numerical precision loss in control systems implemented using fixed and floating point numbers. Finally, the project addresses the challenge of verifying complex non-linear systems using interval analysis, convex optimization and symbolic decision procedures. The results of this research are available to the community in the form of open-source tools. These tools will directly support the verification of complex systems.The educational impact of the project lies in the integration of the research with a course curriculum centered around the theme of rigorous software engineering for cyber-physical systems. The resulting courses provide valuable training to undergraduate as well as graduate students in the use of advanced verification tools and techniques to ensure safe and reliable design of systems.