随机信息物理系统中基于人工智能的未验证控制器的安全防护结构
Safe-visor Architecture for Sandboxing (AI-based) Unverified Controllers in Stochastic Cyber-Physical Systems
摘要：
高性能但未经验证的控制器，例如，基于人工智能的（a.k.a.基于人工智能的控制器被广泛应用于信息物理系统（CPS）中，以完成复杂的控制任务。然而，保证CPS的安全性和可靠性与这种控制器是目前非常具有挑战性的，这是至关重要的，在许多现实生活中的安全关键应用。为了应对这一困难，我们在这项工作中提出了一个安全的遮阳板架构，用于在嘈杂的环境中运行的CPS中对未经验证的控制器进行沙箱化。随机CPS）。建议的架构包含一个基于历史的监督员，它检查来自未经验证的控制器的输入，并在系统的功能和安全性之间做出妥协，以及一个安全顾问，当未经验证的控制器危及系统的安全时，提供回退。基于历史的监督器和安全顾问都是基于原始系统与其有限抽象之间的近似概率关系设计的。通过采用这种体系结构，我们提供了正式的概率保证，保持接受语言的确定性有限自动机（DFA）表示的安全规范。同时，未经验证的控制器仍然可以在控制回路中使用，即使他们是不可靠的。我们证明了我们提出的结果的有效性，将它们应用到两个（物理）的案例研究。
英文摘要：
High performance but unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, are widely employed in cyber-physical systems (CPSs) to accomplish complex control missions. However, guaranteeing the safety and reliability of CPSs with this kind of controllers is currently very challenging, which is of vital importance in many real-life safety-critical applications. To cope with this difficulty, we propose in this work a Safe-visor architecture for sandboxing unverified controllers in CPSs operating in noisy environments (a.k.a. stochastic CPSs). The proposed architecture contains a history-based supervisor, which checks inputs from the unverified controller and makes a compromise between functionality and safety of the system, and a safety advisor that provides fallback when the unverified controller endangers the safety of the system. Both the history-based supervisor and the safety advisor are designed based on an approximate probabilistic relation between the original system and its finite abstraction. By employing this architecture, we provide formal probabilistic guarantees on preserving the safety specifications expressed by accepting languages of deterministic finite automata (DFA). Meanwhile, the unverified controllers can still be employed in the control loop even though they are not reliable. We demonstrate the effectiveness of our proposed results by applying them to two (physical) case studies.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
