From Communicating Machines to Graphical Choreographies

Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. This paper presents an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs). Our results include: a sound and complete characterisation of a subset of safe CFSMs from which global graphs can be constructed; an algorithm to translate CFSMs to global graphs; a time complexity analysis; and an implementation of our theory, as well as an experimental evaluation. Keywords multiparty session types, choreography, communicating finite-state machines, global graphs, theory of regions

• Type: Journal
• Year: 2015
• Where: POPL
• Authors: Julien Lange, Emilio Tuosto, Nobuko Yoshida
• Keywords: POPL 2015, Programming Languages