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

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