基于 STREL 的信息物理系统空间弹性形式化

弹性是系统从违规状态中快速恢复（可恢复性）并尽可能长时间避免未来违规（耐久性）的能力。在空间设定下，可恢复性与耐久性（现称为持续性）以距离为单位进行度量。与其时间对应概念一样，空间弹性对信息物理系统（CPS）具有根本重要性，但迄今为止，尚无广泛达成共识的空间弹性形式化处理方法。我们提出了一个用于推理 CPS 中空间弹性的形式化框架。该框架基于 STREL 的空间片段，我们将其称为 SREL。在此框架中，空间弹性以空间弹性规范的形式给出了语法刻画。SpaRS 的原子谓词称为 S-atom。给定任意 SREL 公式 $\varphi$ 及距离边界 $d_1, d_2$，$\varphi$ 的 S-atom $S_{d_1, d_2} (\varphi)$ 为 SREL 公式 $\neg\varphi R_{[0,d_1]} (\varphi R_{[d_2, +\infty)}\varphi)$，规定从 $\varphi$ 的违规中恢复须在距离 $d_1$ 内发生（可恢复性），随后 $\varphi$ 须沿路径维持大于 $d_2$ 的距离（持续性）。S-atom 可使用空间 STREL 算子进行组合，从而表达复合弹性规范。我们以空间弹性值函数 $\sigma$ 的形式定义了 SpaRS 的定量语义，并证明了其相对于 SREL 布尔语义的可靠性与完备性。$S_{d_1,d_2}(\varphi)$ 的 $\sigma$ 值是一组非支配的 对，用于量化可恢复性与持续性，因为某些路径可能提供更好的可恢复性，而其他路径提供更好的持续性。此外，我们设计了评估 SpaRS 公式 SpaRV 的算法。最后，两个案例研究展示了我们方法的实用价值。