Technical-Report: Automating Recoverability Proofs for Cyber-Physical Systems with Runtime Assurance Architectures

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