CPS: Synergy: Collaborative Research: Formal Models of Human Control and Interaction with Cyber-Physical Systems

网络物理系统（CPS）包括各种各样的系统，例如未来能源系统（例如智能电网）、国土安全和应急响应、智能医疗技术、智能汽车和航空运输。在网络物理系统的设计和部署中，最重要的挑战之一是如何正式地保证它们能够适应有效的人类控制。这是一个具有挑战性的问题，不仅因为未来CPS的操作变化和日益增加的复杂性，而且因为在现实假设下人类-CPS系统的非线性性质。目前的技术水平通常产生了简化的模型，并没有充分考虑到关于系统和环境约束或人类认知能力和局限性的现实假设。为了克服目前最先进的限制，我们的总体研究目标是为复杂的人类cps开发一个理论框架，使正式的分析和验证能够确保整个系统运行的稳定性，并避免不安全的运行状态。要分析涉及有限理性的人类操作员的人类-CPS，需要确定三个关键问题：(a)操作员可用的输入是否足以为CPS产生理想的行为？(b)如果是这样，对于认知有限的操作员来说，将系统推向预期的行为有多容易？(c)如何正式确定系统表现不佳的领域并确定适当的缓解措施？总体技术方法将是(a)开发并适当利用包含人类局限性和能力的一般认知模型，(b)开发抽象认知模型的方法，以产生可处理的分析人类模型(c)开发创新技术，设计人类和底层系统之间的抽象接口，以反映相互约束。(d)扩展当前最先进的可达性和验证算法，用于分析抽象接口，其中反馈回路中的一个系统（即用户）大多是未知的、不确定的、高度可变的或建模不良的。本研究将在以下领域作出具有广泛意义的贡献：(1)基本原理和算法，这些原理和算法将作为人类-CPS混合控制系统的可证明安全的鲁棒混合控制系统的基础；(2)用于开发分析人类模型的方法，该模型包含了人类控制CPS的认知能力和局限性及其后果；(3)经过验证的界面设计技术，通过确保人类安全控制CPS所需的最少信息的界面，实现有效的人类态势感知；(4)可扩展的新可达性分析技术，允许快速确定不同级别的系统安全。该研究将有助于在构建、测试和部署CPS之前识别安全关键、高风险或昂贵的CPS中的问题（例如自动化意外、用户界面中包含的信息不足或过多）。该研究将为理解和发展人类cps提供正式的基础，并将在医疗保健、能源、空中交通管制、运输系统、国土安全和大规模应急响应等领域具有广泛的应用。该研究将通过教育创新和推广，为STEM领域中代表性不足的学生的进步做出贡献。代码、基准和数据将通过项目网站发布。人类认知模型的形式化描述通常与人类操作员控制的网络物理系统（CPS）的形式化模型不兼容。因此，很难以严格的方式确定由人工操作人员控制的CPS是否安全或稳定，以及在何种情况下。本研究的目的是开发一个人类- cps系统的分析框架，该框架包含人类操作员的工程兼容的形式模型，这些模型保留了人类认知的基本架构特征。在这个项目中，小组将开发建立这种模型的方法，以及对人- cps系统进行正式核查的技术，以便提供性能保证。他们将验证各种领域的模型，从空中交通管制到大规模应急响应，再到麻醉管理。

Cyber-Physical Systems (CPS) encompass a large variety of systems including for example future energy systems (e.g. smart grid), homeland security and emergency response, smart medical technologies, smart cars and air transportation. One of the most important challenges in the design and deployment of Cyber-Physical Systems is how to formally guarantee that they are amenable to effective human control. This is a challenging problem not only because of the operational changes and increasing complexity of future CPS but also because of the nonlinear nature of the human-CPS system under realistic assumptions. Current state of the art has in general produced simplified models and has not fully considered realistic assumptions about system and environmental constraints or human cognitive abilities and limitations. To overcome current state of the art limitations, our overall research goal is to develop a theoretical framework for complex human-CPS that enables formal analysis and verification to ensure stability of the overall system operation as well as avoidance of unsafe operating states. To analyze a human-CPS involving a human operator(s) with bounded rationality three key questions are identified: (a) Are the inputs available to the operator sufficient to generate desirable behaviors for the CPS? (b) If so, how easy is it for the operator with her cognitive limitations to drive the system towards a desired behavior? (c) How can areas of poor system performance and determine appropriate mitigations be formally identified? The overall technical approach will be to (a) develop and appropriately leverage general cognitive models that incorporate human limitations and capabilities, (b) develop methods to abstract cognitive models to yield tractable analytical human models (c) develop innovative techniques to design the abstract interface between the human and underlying system to reflect mutual constraints, and (d) extend current state-of-the-art reachability and verification algorithms for analysis of abstract interfaces, iin which one of the systems in the feedback loop (i.e., the user) is mostly unknown, uncertain, highly variable or poorly modeled.The research will provide contributions with broad significance in the following areas: (1) fundamental principles and algorithms that would serve as a foundation for provably safe robust hybrid control systems for mixed human-CPS (2) methods for the development of analytical human models that incorporate cognitive abilities and limitations and their consequences in human control of CPS, (3) validated techniques for interface design that enables effective human situation awareness through an interface that ensures minimum information necessary for the human to safely control the CPS, (4) new reachability analysis techniques that are scalable and allow rapid determination of different levels of system safety. The research will help to identify problems (such as automation surprises, inadequate or excessive information contained in the user interface) in safety critical, high-risk, or expensive CPS before they are built, tested and deployed. The research will provide the formal foundations for understanding and developing human-CPS and will have a broad range of applications in the domains of healthcare, energy, air traffic control, transportation systems, homeland security and large-scale emergency response. The research will contribute to the advancement of under-represented students in STEM fields through educational innovation and outreach. The code, benchmarks and data will be released via the project website.Formal descriptions of models of human cognition are in general incompatible with formal models of the Cyber Physical System (CPS) the human operator(s) control. Therefore, it is difficult to determine in a rigorous way whether a CPS controlled by a human operator will be safe or stable and under which circumstances. The objective of this research is to develop an analytic framework of human-CPS systems that encompasses engineering compatible formal models of the human operator that preserve the basic architectural features of human cognition. In this project the team will develop methodologies for building such models as well as techniques for formal verification of the human-CPS system so that performance guarantees can be provided. They will validate models in a variety of domains ranging from air traffic control to large scale emergency response to the administration of anesthesia.