From Communicating Machines to Graphical Choreographies

Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as fork- ing, merging, and joining for representing application-level proto- cols. Global graphs can be directly translated into modelling nota- tions 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 characteri- sation 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.