运行时强制防护罩的规范说明与最优反应式合成
计算机科学中的逻辑
2019-09-19 v1 形式语言与自动机理论
计算机科学与博弈论
摘要
具有偶发错误的系统（SSE）是一种产生高质量输出但可能偶尔违反关键需求 REQ(I,O) 的控制器。运行时强制防护罩是一种控制器，它接收（来自 SSE 的）(I,O) 作为输入，并产生修正后的输出 O'，以保证需求 REQ(I,O') 的不变性。此外，输出序列 O' 必须“尽可能小地”偏离 O 以维持质量。在本文中，我们给出一种使用量化离散时段演算（QDDC）逻辑公式对防护罩进行逻辑规范说明的方法。该规范说明包含一个正确性需求 REQ 以及一个硬偏离约束 HDC，二者均须被防护罩强制且不变地满足。此外，我们还使用量化优化来给出以 H-最优方式最小化累积偏离期望值的防护罩。我们展示了如何实现软需求引导合成的工具 DCSynth 可用于从给定规范自动合成防护罩。接着，我们给出逻辑公式来规范说明若干防护罩概念，包括 Bloem 等人的 k-稳定化防护罩、Wu 等人的突发错误防护罩，以及一种新的 e,d-防护罩。所有这些规范说明下的防护罩均可使用工具 DCSynth 自动合成。我们给出实验结果，展示我们的防护罩合成工具相对于先前工作的性能。我们还比较了在不同硬偏离约束下合成的防护罩在期望偏离和最坏情况突发偏离延迟方面的性能。
引用
@article{arxiv.1909.08541,
title = {Specification and Optimal Reactive Synthesis of Run-time Enforcement Shields},
author = {Paritosh K. Pandya and Amol Wakankar},
journal= {arXiv preprint arXiv:1909.08541},
year = {2019}
}
备注
In Proceedings GandALF 2019, arXiv:1909.05979. arXiv admin note: text overlap with arXiv:1905.11157