Shield Synthesis: Runtime Enforcement for Reactive Systems
Shield Synthesis: Runtime Enforcement for Reactive Systems
复制标题
Shield Synthesis：反应式系统的运行时执行
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Chao Wang
中科院分区：
文献类型：
--
作者：
R. Bloem;Bettina Könighofer;Robert Könighofer;Chao Wang
可扩展性问题可能会阻止用户验证复杂硬件设计的关键属性。在这种情况下，我们建议合成一个“安全盾”，附加到设计，以加强在运行时的属性。屏蔽合成可以在模型检查和反应合成失败的地方成功，因为它只考虑一小部分关键特性，而不是复杂的设计，或者反应合成的情况下的完整规范。屏蔽持续监控设计的输入/输出，并仅在必要时纠正其错误输出，并且尽可能少，因此可能保留其他非关键属性。虽然在其他领域（如动作系统）中已经研究了运行时执行，但反应式系统提出了独特的挑战，其中屏蔽必须立即行动。因此，我们提出了反应式硬件系统的第一个屏蔽合成解决方案，并报告了我们的实验结果。这是[5]的扩展版本，增加了一个附录。
Scalability issues may prevent users from verifying critical properties of a complex hardware design. In this situation, we propose to synthesize a "safety shield" that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model checking and reactive synthesis fail, because it only considers a small set of critical properties, as opposed to the complex design, or the complete specification in the case of reactive synthesis. The shield continuously monitors the input/output of the design and corrects its erroneous output only if necessary, and as little as possible, so other non-critical properties are likely to be retained. Although runtime enforcement has been studied in other domains such as action systems, reactive systems pose unique challenges where the shield must act without delay. We thus present the first shield synthesis solution for reactive hardware systems and report our experimental results. This is an extended version of [5], featuring an additional appendix.