第2类合同的可实现性检验
Realizability Checking of Contracts with Kind 2
摘要：
我们提出了开源模型检查器Kind 2的一个新特性，它检查组件契约是否可实现;即，有可能构造一个组件，使得对于合同假设所允许的任何输入，存在该组件可以产生的满足合同保证的某个输出值。当合约被证明是不可实现的，它提供了一个死锁计算和一组相互冲突的保证。这个新特性可以用来检测组件规范中的缺陷，并确保Kind 2的组合证明参数的正确性。
英文摘要：
We present a new feature of the open-source model checker Kind 2 which checks whether a component contract is realizable; i.e., it is possible to construct a component such that for any input allowed by the contract assumptions, there is some output value that the component can produce that satisfies the contract guarantees. When the contract is proven unrealizable, it provides a deadlocking computation and a set of conflicting guarantees. This new feature can be used to detect flaws in component specifications and to ensure the correctness of Kind 2's compositional proof arguments.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
