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.

Interface Automata for Choreographies

Emilio Tuosto
2019

Abstract

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.
cs.FL
cs.FL
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/20.500.12571/10244
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact