Interface Automata for Choreographies

Choreographic approaches to message-passing applications can be regarded asan instance of the model-driven development principles. Choreographies specifyinteractions among distributed participants coordinating among themselves withmessage-passing at two levels of abstractions. A global view of the applicationis specified with a model that abstracts away from asynchrony while a localview of the application specifies the communication pattern of eachparticipant. Noteworthy, the latter view can typically be algorithmicallyobtained by projection of the global view. A crucial element of this approachis to verify the so-called well-formed conditions on global views so that itsprojections realise a sound communication protocol. We introduce a novel localmodel, group interface automata, to represent the local view of choreographiesand propose a new method to verify the well-formedness of globalchoreographies. We rely on a recently proposed semantics of global viewsformalised in terms of pomsets.