基于有效性引导的从假设-保证契约综合反应式系统

从规范自动综合反应式系统数十年来一直是研究课题。最近，人们提出多种方法将反应式系统的综合从命题规范扩展到丰富理论上的规范。我们提出一种新颖的、完全自动化的程序综合方法，将问题归约为判定一组全称-存在公式的有效性。受 IC3 / PDR 启发，我们的问题空间通过阻断不安全状态区域递归细化，旨在发现描述安全反应的不动点。若找到这样的不动点，我们构造一个见证并直接转化为实现。我们在 JKind 模型检验器上实现了该算法，并使用 Lustre 规范语言编写的契约对其进行测试。实验结果表明，新算法优于 JKind 已有的基于 k-归纳的综合过程，并解决了 k-归纳方法在不可实现结果方面的可靠性问题。