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
}