Amending Contracts for Choreographies

TL;DR

This paper introduces three automatic methods to correct inconsistent global assertions in choreographies, ensuring valid distributed interactions while maintaining the original contract intentions.

Contribution

It presents novel automated correction techniques for inconsistent global assertions in choreographies, enhancing the reliability of distributed protocol specifications.

Findings

Three correction methods are proposed and compared.

The methods improve consistency of global assertions.

Relationships between amended and original assertions are analyzed.

Abstract

Distributed interactions can be suitably designed in terms of choreographies. Such abstractions can be thought of as global descriptions of the coordination of several distributed parties. Global assertions define contracts for choreographies by annotating multiparty session types with logical formulae to validate the content of the exchanged messages. The introduction of such constraints is a critical design issue as it may be hard to specify contracts that allow each party to be able to progress without violating the contract. In this paper, we propose three methods that automatically correct inconsistent global assertions. The methods are compared by discussing their applicability and the relationships between the amended global assertions and the original (inconsistent) ones.