Title
From Communicating Machines to Graphical Choreographies
Abstract
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.
Year
DOI
Venue
2015
10.1145/2676726.2676964
POPL
Keywords
Field
DocType
communicating finite-state machines,process models,formal definitions and theory,choreography,multiparty session types,theory of regions,global graphs
Graph,Asynchronous communication,Notation,Programming language,Unified Modeling Language,Computer science,Theoretical computer science,Choreography,Merge (version control),Time complexity,Business Process Model and Notation
Conference
Volume
Issue
ISSN
50
1
0362-1340
Citations 
PageRank 
References 
33
0.98
22
Authors
3
Name
Order
Citations
PageRank
J. Lange1422.21
Emilio Tuosto249942.62
Nobuko Yoshida3331.32