Generating accurate runtime safety estimates for autonomous systems is vital to ensuring their continued proliferation. However, accurately reasoning about future system behaviors is generally too complex to do at runtime. To better reason about system safety at runtime, we propose a method for leveraging design time model checking results at runtime. Specifically, we model the system as a probabilistic automaton (PA) and compute bounded time reachability probabilities over the states of the PA at design time. At runtime, we combine distributions of state estimates with the safety probabilities from design time to produce a bounded time safety estimate. We argue that our approach produces well calibrated safety probabilities, assuming the estimated state distributions are well calibrated. We evaluate our approach using a case study of simulated water tanks.

翻译：为自主系统生成准确的运行时安全估计对于确保其持续发展至关重要。然而，准确推理未来系统行为通常过于复杂，难以在运行时实现。为了在运行时更好地推理系统安全性，我们提出了一种在运行时利用设计时模型检测结果的方法。具体而言，我们将系统建模为概率自动机（PA），并在设计时计算PA状态上的有界时间可达概率。在运行时，我们将状态估计的分布与设计时的安全概率相结合，以生成有界时间安全估计。我们论证，若状态估计分布校准良好，该方法可产生校准良好的安全概率。我们通过模拟水箱案例研究评估了该方法。