MobilityReadingGroup

π-calculus, Session Types research at Imperial College

From communicating machines to graphical choreographies
Julien LANGE , Emilio TUOSTO , Nobuko YOSHIDA
42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015) p. 221 - 232

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}},
  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
}