论文标题
与KINT 2的合同的可靠性检查
Realizability Checking of Contracts with Kind 2
论文作者
论文摘要
我们提供了开源模型检查器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.
