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.