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.
The tool is available on this bitbucket repository.
The purpose of this page is to give instructions to reproduce the results summarised in Table 1 (page 9) of the paper. These benchmarks were executed on a 3.40GHz Intel i7 CPU with 16GB of RAM, a virtual machine will give slightly higher execution times. Below, we describe four scripts which, for each benchmark protocol, measure the time it takes to check whether the protocol is GMC and build its corresponding global graph.
There are two alternatives for testing the tool, you can either use a virtual machine -- with the tool (and all its dependencies) pre-installed -- or download and compile the source code directly; see below.
The easiest way to evaluate our tool is to use this virtual machine, size = 1.2G; md5sum = 8bcf5200b1bc77ef7f5ff84dff11a532.
The graphical outputs (.svg files) generated by the tool will appear in the POPL-AEC/outputs folder. Note that the outputs of, e.g., AEC_bench1.py will be overwritten by, e.g., AEC_bench2.py.
If you would like to test your own protocol, use ./rungmc.py <path-to-your-protocol> details on the input format is available in the README file.
The virtual machine has been created and tested on VirtualBox 4.3.16