Numerical Algorithms for Verification, Design, Analysis and Operation of Shared Control Cyber-Physical Systems

共享控制信息物理系统验证、设计、分析和操作的数值算法

• 批准号: RGPIN-2017-04543
• 负责人: Mitchell, Ian
• 金额: $ 2.48万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=710452
• 关键词: Numerical; Algorithms; Verification; Design; Analysis

Objectives: The proposed research is part of a multi-year program to develop numerical algorithms and implementations for the verification, synthesis and design of safe controllers and planners for cyber-physical systems subject to uncertainty arising from the influence of external agents whose behaviour is revealed at run-time. Examples of this often non-random uncertainty include human-in-the-loop control and systems using legacy or independently designed black-box controllers whose safety properties cannot be guaranteed. The techniques developed will maintain safety and support pursuit of the agent's goal in a manner that aligns with user expectations. The research will be informed by shared control applications in powered wheelchairs for cognitively impaired older adults, automated delivery of anesthesia, unmanned aerial vehicles, and collaborative manufacturing. Approach: The foundation of this research is development of numerical algorithms for approximating reachability of systems with continuous or hybrid state models, and in particular algorithms which can generate results robust to model uncertainty. The goal of this algorithm development is not just verification, but rather characterization of the set of control inputs which lead to correct behaviors. The second element of this research program will be to design interventions that use this information to maintain safety or assist the agent to attain its goal, despite uncertainty about that goal and system state. The affective outcome of these interventions on the system's user will be a key feature in their design Expected Significance: Unexpected and incorrect operation can lead to a host of negative consequences, and the potential significance of bad behaviours and/or outcomes is increasing as we transition to human-in-the-loop scenarios and/or compose controllers with poorly understood safety characteristics into complex systems. By developing formal verification methods which can treat online input sources in a black-box fashion, my research program will increase the confidence of designers and users that these systems will perform correctly. By considering how these problems are best solved in a diverse set of application areas, approaches which are more broadly applicable can be identified and subsequently extended to other domains in which cyber-physical systems are prominent. Trainees will gain experience in numerical algorithms, robust software development practices, health care technology development and/or robotics, which are all areas with positive job prospects.

目的：拟议的研究是一项多年计划的一部分，旨在开发数值算法和实施，以验证，合成和设计安全控制器和计划者针对网络物理系统的验证和计划，这些系统受到不确定性，这些系统因在运行时表现出的行为的影响而产生不确定性。这种通常非随机不确定性的示例包括使用遗产或独立设计的黑盒控制器的人类在循环控制和系统，这些控制器无法保证其安全性能。开发的技术将以与用户期望保持一致的方式来维持对代理商目标的安全和支持。这项研究将通过用于认知障碍的老年人，麻醉，无人驾驶飞机和协作制造的自动化的老年人，自动化的老年人的共享控制应用程序来告知这项研究。 方法：这项研究的基础是开发具有连续或混合状态模型的系统的数值算法，尤其是算法，这些算法可以生成可靠的结果以模拟不确定性。该算法开发的目的不仅是验证，而且还表征导致纠正行为的控制输入集。 该研究计划的第二个要素是设计干预措施，尽管对该目标和系统状态不确定，但使用此信息来维持安全或协助代理商实现其目标。 这些干预措施对系统用户的情感结果将是其设计的关键功能 预期的意义：意外的和错误的操作会导致许多负面后果，并且随着我们过渡到人类的环境和/或组成的控制器，不良行为和/或结果的潜在意义正在增加，而安全特征却不理解为复杂的系统。通过开发可以以黑盒方式处理在线输入来源的正式验证方法，我的研究计划将增加设计人员和用户这些系统将正确性能的信心。 通过考虑如何在各种应用领域中最好地解决这些问题，可以识别出更广泛适用的方法，然后将其扩展到网络物理系统突出的其他领域。 受训人员将获得数值算法，健壮的软件开发实践，医疗保健技术开发和/或机器人技术的经验，这些领域都是有积极的工作前景的领域。