使用可实现性 Skolem 化证明的 Assume-Guarantee 契约综合

需求工程中的可实现性问题旨在确定是否存在满足给定形式需求的实现。证明可实现性之后向前迈出的一步是自动构造这样的实现，从而解决程序综合问题。在本文中，我们提出了一种由从安全性质构造的 assume-guarantee 契约的 k-归纳可实现性证明指导的程序综合新方法。可实现性证明在一组 forall-exists 公式上进行，综合则通过提取见证存在量化的 Skolem 函数来执行。然后可以将这些 Skolem 函数组合成一个实现。我们的方法在 JSyn 工具中实现，该工具从用 Lustre 编程语言变体编写的契约中构造 Skolem 函数，然后将 Skolem 函数编译为 C 语言实现。对于已经包含手写实现的各种基准模型，在假设基于组件的验证框架下，我们能够识别所综合对应物的可用性和有效性。