From Communicating Machines to Graphical Choreographies
Open Access
- 14 January 2015
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
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.Keywords
Funding Information
- Seventh Framework Programme (FP7-612985,FP7-295261)
- Engineering and Physical Sciences Research Council (EP/K034413/1,EP/K011715/1,EP/L00058X/1)
This publication has 24 references indexed in Scilit:
- Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session TypesLecture Notes in Computer Science, 2013
- On Global Types and Multi-Party SessionLogical Methods in Computer Science, 2012
- Weak bisimulation for Probabilistic Timed AutomataTheoretical Computer Science, 2010
- Verification of programs with half-duplex communicationInformation and Computation, 2005
- Inference of message sequence chartsIEEE Transactions on Software Engineering, 2003
- Synthesizing Distributed Finite-State Systems from MSCsLecture Notes in Computer Science, 2000
- Deriving Petri nets from finite transition systemsInternational Conference on Acoustics, Speech, and Signal Processing (ICASSP), 1998
- Theory of regionsLecture Notes in Computer Science, 1998
- Protocol specifications and component adaptorsACM Transactions on Programming Languages and Systems, 1997
- On Communicating Finite-State MachinesJournal of the ACM, 1983