From Orchestration to Choreography through Contract Automata

TL;DR

This paper explores the relationship between contract automata and interaction models, establishing a formal connection that ensures well-formed choreographies from strong agreements in distributed service coordination.

Contribution

It introduces a formal mapping from contract automata to interaction models and defines conditions linking strong agreement to choreography correctness.

Findings

Established a formal mapping between contract automata and interaction models

Defined strong agreement and its relation to choreography correctness

Provided conditions ensuring well-formed choreographies from contract automata

Abstract

We study the relations between a contract automata and an interaction model. In the former model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The interaction model relies on channel-based asynchronous communication and choreography to coordinate distributed services. We define a notion of strong agreement on the contract model, exhibit a natural mapping from the contract model to the interaction model, and give conditions to ensure that strong agreement corresponds to well-formed choreography.