Cyber-physical systems (CPSes), such as autonomous vehicles, use sophisticated components like ML-based controllers. It is difficult to provide evidence about the safe functioning of such components. To overcome this problem, Runtime Assurance Architecture (RTA) solutions have been proposed. The \RAP's decision component evaluates the system's safety risk and whenever the risk is higher than acceptable the RTA switches to a safety mode that, for example, activates a controller with strong evidence for its safe functioning. In this way, RTAs increase CPS runtime safety and resilience by recovering the system from higher to lower risk levels. The goal of this paper is to automate recovery proofs of CPSes using RTAs. We first formalize the key verification problems, namely, the decision sampling-time adequacy problem and the time-bounded recoverability problem. We then demonstrate how to automatically generate proofs for the proposed verification problems using symbolic rewriting modulo SMT. Automation is enabled by integrating the rewriting logic tool (Maude), which generates sets of non-linear constraints, with an SMT-solver (Z3) to produce proofs

翻译：信息物理系统（CPS），例如自动驾驶车辆，采用了诸如基于机器学习的控制器等复杂组件。为这些组件的安全运行提供证据十分困难。为解决此问题，研究者提出了运行时保证架构（RTA）方案。RTA的决策组件评估系统的安全风险，当风险超过可接受水平时，RTA切换至安全模式（例如，激活具备强安全性证据的控制器）。通过这种方式，RTA将系统从高风险水平恢复至低风险水平，从而提升CPS的运行时安全性和弹性。本文旨在实现基于RTA的CPS可恢复性证明的自动化。首先，我们形式化了关键验证问题，即决策采样时间充足性问题与时间有界可恢复性问题。随后，我们展示了如何通过基于SMT的符号重写方法自动生成针对所述验证问题的证明。自动化实现依赖于将重写逻辑工具（Maude）与SMT求解器（Z3）集成：Maude生成非线性约束集合，Z3则生成证明。