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

目标：这项拟议的研究是一个多年计划的一部分，该计划旨在开发数字算法和实现，用于验证、综合和设计网络物理系统的安全控制器和规划器，这些系统受到外部代理的影响，这些外部代理的行为在运行时被揭示。这种通常非随机不确定性的例子包括人在回路控制和使用传统的或独立设计的黑盒控制器的系统，这些控制器的安全性能无法保证。开发的技术将保持安全性，并支持以符合用户期望的方式追求代理的目标。这项研究将从为认知受损的老年人提供动力轮椅的共享控制应用程序、麻醉的自动输送、无人驾驶飞行器和协作制造中获得信息。*方法：这项研究的基础是开发数值算法来近似具有连续或混合状态模型的系统的可达性，特别是能够产生对模型不确定性稳健的结果的算法。该算法开发的目标不仅是验证，而且是对导致正确行为的一组控制输入的表征。这项研究计划的第二个要素将是设计使用这些信息来维护安全或帮助代理人实现其目标的干预措施，尽管该目标和系统状态不确定。这些干预措施对系统用户的情感结果将是其设计的一个关键特征*预期意义：意外和不正确的操作可能导致一系列负面后果，随着我们过渡到人在回路场景和/或将缺乏理解的安全特性的控制器组合成复杂系统，不良行为和/或结果的潜在意义正在增加。通过开发能够以黑盒方式处理在线输入源的正式验证方法，我的研究计划将增加设计人员和用户对这些系统将正确运行的信心。通过考虑如何在不同的应用领域最好地解决这些问题，可以确定更广泛适用的方法，并随后将其扩展到网络物理系统突出的其他领域。学员将在数值算法、强大的软件开发实践、医疗保健技术开发和/或机器人方面获得经验，这些领域都有积极的就业前景。

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.******