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

CSR：小型：协作研究：使用优化和最优控制技术对复杂信息物理系统进行灰盒测试

• 批准号: 1319457
• 负责人: Sriram Sankaranarayanan
• 金额: $ 24.94万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-10-01 至 2016-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319457&HistoricalAwards=false
• 关键词: CSR; Small; Collaborative; Research; Gray

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.

该项目开发了用于测试复杂的网络物理系统的新方法，这些方法可以在各种应用领域（例如汽车，空域，医疗设备和发电）中执行安全至关重要的任务。这些应用程序中的主要挑战在于物理系统的复杂性，其建模为具有大量状态变量的非线性普通微分方程（ODE）的系统，以及该物理子系统与基于软件的控制器的相互作用。在许多工业应用中，这些模型甚至在封闭形式的表示中都无法使用，并且只能执行系统模拟。在这个项目中，采用了优化和最佳控制理论的想法，以推动国家空间探索的过程进行系统验证。时间逻辑规格的鲁棒性指标理论与非平滑优化理论结合使用，该理论导致多模式CP的梯度下降搜索方法。在更高级别上，将混凝土和符号执行技术组合在一起，以增强搜索方法的性能。验证方法可以很容易地集成到现有的工业强度模拟环境中。此类验证工具的目标应用程序来自医疗和汽车应用领域。复杂CPS的验证是一个具有挑战性的问题。由于几乎所有制造商的软件错误都确立了问题的紧迫性和重要性，因此对医疗和汽车产品的持续和多次召回。该项目导致集成在现有且广泛采用的基于模型的开发平台内​​的可用验证工具。该应用集中在医疗和汽车软件的验证上，最终有助于避免由于这些安全至关重要系统中的错误而造成的有害损失。对社会的具体益处是双重的：首先，改善了系统安全性和可靠性；其次，减少了新产品的开发时间。该项目的教育方面围绕着培训学生的基于模型的设计和针对安全至关重要的CP的验证方法的课程。该项目的教育任务还强调了设计CPS的“安全性第一”方法，其中规范和验证被教授为设计中不可或缺的步骤，而不是设计后的步骤。除研究出版物外，传播途径还包括通过cps-vo.org和其他公共访问网站共享软件，模型和课程材料。