CAREER:Robust Verification of Cyber-Physical Systems

网络物理系统（cps）在现代社会中已经变得无处不在，在交通、医疗和能源领域实现了变革性的应用。然而，cps的可靠开发仍然是一个突出的挑战。在设计层面，混合系统理论提供了一套丰富的技术和工具，以确保安全性和活动性等高级功能属性的正确性。当前实现级别的分析技术主要关注于检测低级运行时错误，如缓冲区溢出和除零。验证功能规格说明的整体方法将大大提高cps开发的可靠性。该项目研究了一种健壮的验证方法，该方法通过对设计进行“更深入”的分析来保证实现的功能正确性。更准确地说，健壮的验证不仅确保设计满足给定的规范，而且确保设计中的小扰动仍然满足规范。设计上的扰动解释了实现中相对于实际系统的偏差。根据鲁棒性的新颖定量和/或拓扑方面，提出的研究调查了鲁棒分析的新基础，抽象和验证算法。此外，还开发了原型工具，以实现实际应用和评估。该研究的成功完成将通过利用控制理论、动力系统理论、优化理论和可满足模理论的思想，推进形式方法和混合控制系统领域的知识。在混合控制系统设计和分析的本科和研究生阶段将开发和教授新的跨学科课程。为大学预科学生举办的涉及物理系统编程的活动将增加他们对STEM相关职业的兴趣。本科生，特别是来自少数民族和代表性不足群体的本科生，将通过参与研究和外联活动来征聘和指导。这项研究的成功将通过弥合设计和实施阶段分析的差距，迫使cps的现有验证方法发生巨大飞跃，特别是在汽车和航空航天系统领域。

Cyber-physical systems (CPSs) have become pervasive in the modern society, enabling transformative applications in the transportation, healthcare and energy sectors. However, the reliable development of CPSs remains an outstanding challenge. At the design level, hybrid systems theory provides a rich set of techniques and tools for ensuring correctness of high level functional properties such as safety and liveness. Current analysis techniques at the implementation level focus primarily on detecting low level runtime errors such as buffer overflows and divide by zero. A holistic approach to verifying functional specifications will considerably enhance the reliability scenario of CPSs development. This project investigates a robust verification methodology that guarantees functional correctness of the implementation by a "deeper" analysis on the design. More precisely, robust verification not only ensures that a design satisfies a given specification, but that small perturbations in the design still satisfy the specification. The perturbations on the design account for the deviations in the implementation with respect to the actual system. The proposed research investigates new foundations, abstractions and verification algorithms for robust analysis, in light of novel quantitative and/or topological aspects of robustness. In addition, prototype tools are developed to enable practical application and evaluation. The successful completion of the research will advance the knowledge in the fields of formal methods and hybrid control systems by leveraging ideas from control theory, dynamical systems theory, optimization theory and satisfiability modulo theory.New cross-disciplinary courses at the undergraduate and graduate levels in hybrid control system design and analysis will be developed and taught. Activities for pre-college students involving programming with physical systems will be conducted towards increasing their interest in STEM related careers. Undergraduates, especially those from minority and underrepresented groups, will be recruited and mentored through involvement in research and outreach activities. The success of this research will force a quantum jump in the existing verification methodologies for CPSs, in particular, in the domains of automotive and aerospace systems, by bridging the gap in the analyses at the design and implementation phases.