基于 STL 的信息物理系统弹性形式化

弹性是指从违例快速恢复并尽可能长久避免未来违例的能力。此类性质对信息物理系统（CPS）至关重要，然而迄今尚无广泛认同的 CPS 弹性形式化处理方法。我们提出一个基于 STL 的 CPS 弹性推理框架，其中弹性具有以基于 STL 的弹性规范（SRS）形式的语法刻画。给定任意 STL 公式 $\varphi$、时间界 $\alpha$ 与 $\beta$，$\varphi$ 的 SRS，$R_{\alpha,\beta}(\varphi)$，是 STL 公式 $\neg\varphi\mathbf{U}_{[0,\alpha]}\mathbf{G}_{[0,\beta)}\varphi$，指明 $\varphi$ 的违例应在时间 $\alpha$ 内恢复（可恢复性），随后 $\varphi$ 应保持时长 $\beta$（持久性）。这些 $R$-表达式作为我们 SRS 逻辑中的原子，可使用 STL 算子组合，从而表达复合弹性规范，例如多个 SRS 必须同时成立，或系统最终必须具备弹性。我们为 SRS 定义了以弹性满足值（ReSV）函数 $r$ 形式的定量语义，并证明其相对于 STL 布尔语义的可靠性与完备性。$R_{\alpha,\beta}(\varphi)$ 原子的 $r$-值是一个包含量化可恢复性与持久性之对的单元素集合。复合 SRS 公式的 $r$-值得到一组非支配的可恢复性-持久性对，因为子公式的 ReSV 可能不可直接比较（例如一个子公式持久性更优但可恢复性更差）。据我们所知，这是首个针对基于 STL 逻辑的多维定量语义。两个案例研究展示了我们方法的实际效用。