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

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

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.