Interface Automata for Choreographies

TL;DR

This paper introduces group interface automata as a new local model for choreographies, providing a method to verify well-formed global views in message-passing applications using pomset semantics.

Contribution

It presents a novel local model and verification method for global choreographies, enhancing the analysis of message-passing systems.

Findings

Introduces group interface automata for local choreography modeling

Proposes a new verification method for well-formed global views

Utilizes pomset semantics for formal analysis

Abstract

Choreographic approaches to message-passing applications can be regarded as an instance of the model-driven development principles. Choreographies specify interactions among distributed participants coordinating among themselves with message-passing at two levels of abstractions. A global view of the application is specified with a model that abstracts away from asynchrony while a local view of the application specifies the communication pattern of each participant. Noteworthy, the latter view can typically be algorithmically obtained by projection of the global view. A crucial element of this approach is to verify the so-called well-formed conditions on global views so that its projections realise a sound communication protocol. We introduce a novel local model, group interface automata, to represent the local view of choreographies and propose a new method to verify the well-formedness of global choreographies. We rely on a recently proposed semantics of global views formalised in terms of pomsets.