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),并在设计时计算巴勒斯坦权力机构各州受约束的时间可达性概率。在运行时,我们把国家估算的分布与安全概率结合起来,从设计时间到提出受约束的时间安全估计。我们争论说,我们的方法产生了经过精确校准的安全概率,假设估计的状态分布是经过良好校准的。我们用模拟储水罐的案例研究来评估我们的方法。