CSR: Small: Collaborative Research: Gray Box Testing of Complex Cyber-Physical Systems Using Optimization and Optimal Control Techniques

该项目为测试复杂的网络物理系统开发了新的方法，这些系统在汽车、航空航天、医疗设备和发电等广泛的应用领域执行安全关键任务。这些应用中的主要挑战在于物理系统的复杂性，该物理系统被建模为具有大量状态变量的非线性常微分方程组(ODE)系统，以及该物理子系统与基于软件的控制器的相互作用。在许多工业应用中，这些模型甚至不能以封闭形式表示，只能执行系统仿真。在这个项目中，运用最优化和最优控制理论的思想来驱动系统验证的状态空间探索过程。将时态逻辑规范的稳健性度量理论与非光滑优化理论相结合，提出了多模式CPS的梯度下降搜索方法。在更高的层次上，将具体执行技术和符号执行技术相结合，以增强搜索方法的性能。验证方法可以很容易地集成到现有的工业强度模拟环境中。这类验证工具的目标应用来自医疗和汽车应用领域，复杂CPS的验证是一个具有挑战性的问题。几乎所有制造商都因软件错误而连续多次召回医疗和汽车产品，这证明了问题的紧迫性和重要性。该项目使可用的核查工具集成到现有的和广泛采用的基于模型的开发平台中。该应用程序专注于医疗和汽车软件的验证，最终有助于避免由于这些安全关键系统中的错误而造成的有害损失。对社会的具体好处有两个：第一，提高了系统的安全性和可靠性；第二，减少了新产品的开发时间。这个项目的教育方面围绕着培训学生基于模型的设计和安全关键CP的验证方法的课程。该项目的教育使命还强调“安全第一”的方法来设计CPS，在这种方法中，规范和验证被作为设计中的组成部分而不是设计后的步骤来教授。除了研究出版物，传播途径还包括通过cps-vo.org和其他可公开访问的网站共享软件、模型和课程材料。

The project develops new methodologies for testing complex Cyber-Physical Systems that perform safety-critical tasks in a wide variety of application domains such as automotive, airspace, medical devices and power generation. The primary challenge in these applications lies in the complexity of the physical system, modeled as systems of non-linear Ordinary Differential Equations (ODE) with a large number of state variables, and the interaction of this physical subsystem with a software-based controller. In many industrial applications, these models are not even available in a closed-form representation and only system simulations can be performed. In this project, ideas from optimization and optimal control theory are employed in order to drive the process of state-space exploration for system verification. The theory of robustness metrics for temporal logic specifications is combined with non-smooth optimization theory which results in gradient descent search methods for multi-modal CPS. At a higher level, concrete and symbolic execution techniques are combined to enhance the performance of the search methods. The verification methods can be readily integrated into existing industrial strength simulation environments. The target applications for such verification tools are from the domains of medical and automotive applications.Verification of complex CPS is a challenging problem. Continuous and multiple recalls of medical and automotive products due to software errors across virtually all manufacturers establish the urgency and importance of the problem. This project results in usable verification tools integrated inside existing and widely adopted model-based development platforms. The application focus on the verification of medical and automotive software ultimately helps avoid harmful losses due to errors in these safety-critical systems. The concrete benefit to society is twofold: first, improved system safety and dependability; and, second, reduced development times for new products. The educational aspects of this project revolve around courses that train students on model-based design and verification methods for safety-critical CPS. The educational mission of the project also stresses a "safety first" approach to designing CPS wherein specification and verification are taught as integral steps in the design rather than post-design steps. Besides research publications, avenues of dissemination include sharing of software, models, and course materials via cps-vo.org and other publicly accessible websites.