From Communicating Machines to Graphical Choreographies (pdf)

Introduction

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.

Using the Tool and Generating Benchmarks

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.

1. Using the Virtual Machine

The easiest way to evaluate our tool is to use this virtual machine, size = 1.2G; md5sum = 8bcf5200b1bc77ef7f5ff84dff11a532.

Installation

• decompress GMC-Machine.ova.tar.gz,
• install and start VirtualBox,
• import the GMC-Machine virtual machine image (File > Import Appliance ...),
• start GMC-Machine
• once Ubuntu has started, open a terminal,
• Go to the POPL-AEC directory (i.e., cd POPL-AEC).

Instructions

• ./rungmc.py <path-to-cfsm> runs the tool for a selected example (see tests folder, e.g., ./rungmc.py tests/benchmark/gmc/runningExample will run the tool on the running example in the paper),
• ./AEC_bench1.py will run all the (smaller) benchmark protocols (listed in the paper) and output execution times, based on 1 iteration,
• ./AEC_bench1_30.py will run all the (smaller) benchmark protocols (listed in the paper) and output execution times, based on 30 iterations,
• ./AEC_bench2.py will run all the X2 (bigger) benchmark protocols (listed in the paper) and output execution times, based on 1 iteration,
• ./AEC_bench2_30.py will run all the X2 (bigger) benchmark protocols (listed in the paper) and output execution times, based on 30 iterations.

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

2. Using the Source Code

• run git clone git@bitbucket.org:julien-lange/gmc-synthesis.git or download the source code (and decompress the file),
• install and configure the dependencies listed in ./gmc-synthesis/README,
• compile the tool (cf README),
• the scripts listed above work as in the virtual machine.