CAREER: Robustness Guided Testing and Verification for Cyber-Physical Systems

该项目开发了一个理论框架以及软件工具，以支持基于模型的设计（MBD）过程中的网络物理系统（CPS）的测试和验证。该框架的理论基础是随机优化方法和形式化规范语言的鲁棒性概念。该项目的研究包括三个组成部分：发展条件的算法和结构的CPS推断有限的时间保证的随机测试过程中;测试方法的研究，可以支持模块化和组合系统设计;和调查的适当概念之间的一致性两个系统模型和模型之间，其实现在计算平台上。所有这些组件都需要支持MBD过程所有阶段的测试和验证，以及支持组件重用，增量系统改进和模块化设计。框架的评估是由验证汽车控制系统和医疗设备的问题驱动的。随着安全关键型CPS变得无处不在，对保证正确的系统功能和性能的设计方法的需求变得更加迫切。认证和政府机构需要可靠的测试和验证工具，以纳入认证标准和程序。对社会的具体好处是减少了新产品的灾难性设计错误，并降低了新产品开发的经济成本。前者增加了对新技术的信心，而后者提高了利用这些技术的公司的竞争力。该项目的理论成果正在被纳入软件工具中，用于复杂CPS的测试、验证和确认。该项目的评估重点是验证输液泵和自动控制软件，最终有助于避免由于这些安全关键系统中的错误而造成的有害损失。任何基于正式或半正式方法的软件工具的使用都需要工程师在这些技术方面接受过扎实的培训。该提案提出了一个教育课程，用于开发新课程，在各级高等教育中引入正式和半正式的CPS方法，即，本科、研究生和继续教育。特别注意的是投入到实践工程师谁必须获得新的MBD技能的在线继续教育。

This project develops a theoretical framework as well as software tools to support testing and verification of a Cyber-Physical System (CPS) within a Model-Based Design (MBD) process. The theoretical bases of the framework are stochastic optimization methods, and robustness notions of formal specification languages. The project's research comprises three components: development of conditions on the algorithms and on the structure of the CPS for inferring finite-time guarantees on the randomized testing process; the study of testing methods that can support modular and compositional system design; and investigation of appropriate notions of conformance between two system models and between a model and its implementation on a computational platform. All of these components are needed to support testing and verification in all the stages of an MBD process as well as to support component reuse, incremental system improvements and modular design. The evaluation of the framework is driven by the problems of verifying automotive control systems and medical devices. As safety-critical CPS become ubiquitous, the need for design methods that guarantee correct system functionality and performance becomes more urgent. Certification and government agencies need dependable testing and verification tools to incorporate in certification standards and procedures. The concrete benefits to the society are both in terms of reduced catastrophic design errors in new products and in terms of reduced economic costs for new product development. The former increases the confidence in new technologies while the latter improves the competitiveness of the companies that utilize such technologies. The theoretical results of this project are being incorporated into software tools for testing, verification and validation of complex CPS. The evaluation focus of the project on verifying infusion pumps and automotive control software ultimately helps in avoiding harmful losses due to errors in these safety-critical systems. The use of any software tool that is based on formal or semi-formal methods requires engineers with solid training on these technologies. This proposal puts forward an education curriculum for developing new courses that introduce formal and semi-formal methods for CPS at all levels of higher education, i.e., undergraduate, graduate and continuing education. Particular attention is devoted into on-line continuing education of practicing engineers who must acquire new MBD skills.