Synthesis of graphical choreographies
File(s)DTR14-4.pdf (691.98 KB)
Published version
Author(s)
Lange, Julien
Yoshida, Nobuko
Tuosto, Emilio
Type
Report
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 synthesised from asynchronous buffered
behaviours 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 synthesised; a synthesis algorithm to translate CFSMs
to global graphs; a time complexity analysis; and an implementation of our theory,
as well as an experimental evaluation.
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 synthesised from asynchronous buffered
behaviours 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 synthesised; a synthesis algorithm to translate CFSMs
to global graphs; a time complexity analysis; and an implementation of our theory,
as well as an experimental evaluation.
Date Issued
2014-01-01
Citation
Departmental Technical Report: 14/4, 2014, pp.1-38
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
38
Journal / Book Title
Departmental Technical Report: 14/4
Copyright Statement
© 2014 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
14/4