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

职业：可靠的分布式网络物理系统的算法和验证

• 批准号: 1054247
• 负责人: Sayan Mitra
• 金额: $ 44.99万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-02-01 至 2018-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1054247&HistoricalAwards=false
• 关键词: CAREER; Algorithms; Verification; Reliable; Distributed

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.

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