Realizability Checking of Contracts with Kind 2

Daniel Larraz; Cesare Tinelli

doi:10.48550/arxiv.2205.09082

Back

Realizability Checking of Contracts with Kind 2

Preprint

Open access

Realizability Checking of Contracts with Kind 2

Daniel Larraz and Cesare Tinelli

ArXiv.org

05/18/2022

DOI: 10.48550/arxiv.2205.09082

Files and links (1)

url

https://doi.org/10.48550/arxiv.2205.09082View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

Abstract

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.

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Realizability Checking of Contracts with Kind 2
Creators: Daniel Larraz
Cesare Tinelli
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2205.09082
ISSN: 2331-8422
Language: English
Date posted: 05/18/2022
Academic Unit: Computer Science
Record Identifier: 9984410856902771

Metrics

2 Record Views