Composition of choreography automata

TL;DR

This paper introduces choreography automata as a compositional model for choreographies, enabling modular design and ensuring well-formedness through a new composition operation.

Contribution

It defines a novel composition operation for choreography automata, allowing modular construction of global views while preserving well-formedness and deadlock-freedom.

Findings

Composition of well-formed choreography automata remains well-formed.

The composition operation supports modular design of choreographies.

Projections of global views are live, lock-free, and deadlock-free.

Abstract

Choreography automata are an automata-based model of choreographies, that we show to be a compositional one. Choreography automata represent global views of choreographies (and rely on the well-known model of communicating finite-state machines to model local behaviours). The projections of well-formed global views are live as well as lock- and deadlock-free. In the class of choreography automata we define an internal operation of {\em composition}, which connects two global views via roles acting as interfaces. We show that under mild conditions the composition of well-formed choreography automata is well-formed. The composition operation enables for a flexible modular mechanism at the design level.