CPS: Breakthrough: Knowledge-Aware Cyber-Physical Systems

CPS：突破：知识感知网络物理系统

• 批准号: 1446712
• 负责人: Andre Platzer
• 金额: $ 49.97万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1446712&HistoricalAwards=false
• 关键词: CPS; Breakthrough; Knowledge; Aware; Cyber

This project addresses the foundational problem of knowledge within cyber-physical systems (CPS), i.e., systems that combine aspects such as communication, computation, and physics. A single system observes its environment through sensors and interacts through actuators. Neither is perfect. Thus, the CPS's internal view of the world is blurry and its actions are imprecise. CPS are still analyzed with methods that do not distinguish between truth in the world and an internal view thereof, resulting in a mismatch between the behavior of theoretical models and their real-world counterparts. How could they be trusted to perform safety-critical tasks? This project addresses this critical insufficiency by developing methods to reason about knowledge and learning in CPS. The project pursues the development of new logical principles for verifying knowledge-aware CPS. This project investigates how to make the mismatch between the world and the partial perception through sensors explicit and how to achieve provably correct control in theory as well as practice despite this mismatch. By investigating changing knowledge in a changing world, this project contributes to a fundamental feature without which CPS can never be truly safe and efficient at the same time. The project's broader significance and importance are a result of the widespread attention that CPS gain in many safety-critical areas, such as in aviation and automotive industries. One reason for safety gaps in such CPS is that formal verification techniques are still largely knowledge-agnostic, and verifiable solutions overly pessimistic. This project addresses these issues and provides tools that allow for incorporating knowledge about the environment's intentions into the models to derive provably correct, but justifiably optimistic, and thus efficient, behavior. By their logical nature, these techniques are applicable to a wide range of CPS and, thus, contribute significantly to numerous applications. Results obtained within this project will be demonstrated in CPS models and laboratory robot scenarios, and will be shared in courses and with industrial partners.The technical approach that this project pursues develops a new modeling language, logic, and proof calculus for verifying knowledge-aware CPS. The knowledge paradigm used allows CPS controllers to seamlessly acquire knowledge about the world but also about other agents in the system, i.e., other controllers. Knowledge is the key to interactions between different agents. This project investigates how an explicit model of world perception and agent intentions - and knowledge of these perceptions and intentions - allows CPS agents to act, based on more efficient, but still provably safe control in multi-agent scenarios. The methods will be implemented in the verification tool KeYmaera and demonstrated in formal verification on different case study applications such as car scenarios.

该项目解决网络物理系统（CPS）（即结合通信、计算和物理等方面的系统）内知识的基本问题。单个系统通过传感器观察其环境并通过执行器进行交互。两者都不完美。因此，CPS 的内部世界观是模糊的，其行动也是不精确的。 CPS 的分析方法仍然不区分世界真相和内部观点，导致理论模型的行为与现实世界的对应物不匹配。如何才能信任他们执行安全关键任务？该项目通过开发推理 CPS 知识和学习的方法来解决这一严重不足。该项目致力于开发新的逻辑原理来验证知识感知的 CPS。该项目研究如何使世界与传感器的部分感知之间的不匹配变得明确，以及如何在这种不匹配的情况下在理论和实践上实现可证明的正确控制。通过研究不断变化的世界中不断变化的知识，该项目提供了一个基本功能，没有这个功能，CPS 永远无法同时实现真正的安全和高效。该项目具有更广泛的意义和重要性，是因为 CPS 在许多安全关键领域（例如航空和汽车行业）获得了广泛关注。这种 CPS 中存在安全漏洞的原因之一是，形式验证技术在很大程度上仍然与知识无关，而可验证的解决方案过于悲观。该项目解决了这些问题，并提供了工具，允许将有关环境意图的知识纳入模型中，以得出可证明正确但合理乐观的高效行为。就其逻辑性质而言，这些技术适用于广泛的 CPS，因此对众多应用做出了重大贡献。该项目获得的结果将在 CPS 模型和实验室机器人场景中进行演示，并将在课程中以及与工业合作伙伴共享。该项目追求的技术方法开发了一种新的建模语言、逻辑和证明演算，用于验证知识感知 CPS。所使用的知识范式允许 CPS 控制器无缝地获取有关世界的知识，以及有关系统中其他代理（即其他控制器）的知识。知识是不同主体之间交互的关键。该项目研究了世界感知和智能体意图的显式模型以及这些感知和意图的知识如何允许 CPS 智能体基于多智能体场景中更有效但仍可证明安全的控制来采取行动。这些方法将在验证工具 KeYmaera 中实施，并在汽车场景等不同案例研究应用的形式验证中进行演示。