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.