CAREER: Algorithms and Verification for Reliable Distributed Cyber-Physical Systems

网络物理系统（CPS）正在成为从交通管理到自动驾驶汽车等许多工程领域的关键推动者。并发性、故障以及它们与物理环境的交互使得从这样的系统中获得高水平的信任具有挑战性。该项目开发了一个可重用的中间件服务，通过向两个方向推动最新技术，可以创建经过验证的可靠的分布式CPS:(1)由于面对动态故障和更改时产生的高通信成本，现有的分布式服务无法实际实现。本项目开发了一种组通信服务（GCS），可以在合理的资源下实现，并保证故障后自动恢复（稳定）。(2)现有的验证技术侧重于非分布式的CPS，并且在具有故障、消息延迟等的一般系统中，不太可能适用于自动化分析。对于使用GCS构建的应用程序，该项目开发了一套验证工具，这些工具利用了应用程序的稳定性、组合性、抽象精化和延迟不敏感性。这些核心研究任务将导致混合和分布式系统的设计和验证的根本进步。该项目的成果有望提高自动驾驶汽车和工厂以及智能监控系统中新兴应用的可靠性，同时通过自动化保持可接受的开发成本。通过行业合作，研究成果将转化为工程实践。教育部分将为研究生、本科生和高中生提供课程和实验模块，目的是统一系统课程中的物理和计算观点。通过积极的招聘和指导，妇女和少数民族学生将为从事科学研究工作做好准备。

Cyber-physical systems (CPS) are becoming the key enabler in many engineering domains from traffic management to autonomous vehicles. Concurrency, failures, and their interactions with the physical environment make it challenging to wrestle a high level of confidence from such systems. This project develops a reusable middleware service which enables the creation of verified and hence reliable distributed CPS by pushing the state-of-the-art in two directions: (1) Existing distributed services cannot be practically implemented because of high communication costs incurred in the face of dynamic failures and changes. This project develops a Group Communication Service (GCS) which can be implemented with reasonable resources and which guarantees automatic recovery after failures (stabilization). (2) Existing verification techniques focus on non-distributed CPS, and in general systems with failures, message delays, etc., are unlikely to be amenable to automated analysis. For applications built with the GCS, the project develops a suite of verification tools that exploit stabilization, compositionality, abstraction-refinement, and delay insensitivity of applications. These core research tasks will lead to fundamental advances in design and verification of hybrid and distributed systems. The outcomes of this project are expected to bolster the dependability of emerging applications in autonomous vehicles and factories, and intelligent surveillance systems, while keeping the development costs acceptable through automation. Through industry collaborations, the research outcomes will be translated into engineering practices. The educational component will provide course and lab modules for graduate, undergraduate, and high-school students with the aim of unifying the physical and the computational viewpoints in the systems curriculum. Through active recruitment and mentoring, women and minority students will be prepared for careers in scientific research.