Realizability Checking of Contracts with 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 satisfie...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2022-05
Main Authors: Larraz, Daniel, Tinelli, Cesare
Format: Article
Language:English
Subjects:
Flaw detection
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422