MobilityReadingGroup

From communicating machines to graphical choreographies

Julien LANGE, Emilio TUOSTO, Nobuko YOSHIDA

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.

@inproceedings{LTY2015,
  author = {Julien Lange and Emilio Tuosto and Nobuko Yoshida},
  title = {{From communicating machines to graphical choreographies}},
  booktitle = {42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages = {221--232},
  publisher = {ACM},
  year = 2015
}

@inproceedings{LTY2015,
  author = {Julien Lange and Emilio Tuosto and Nobuko Yoshida},
  title = {{From communicating machines to graphical choreographies}},
  booktitle = {42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages = {221--232},
  publisher = {ACM},
  doi = "10.1145/2676726.2676964",
  year = 2015
}