Amending Choreographies

Ivan Lanese, Fabrizio Montesi, Gianluigi Zavattaro [2013].
In proceedings of WWV 2013, pp. 34-48.

Choreographies are global descriptions of system behaviors, from which the local behavior of each endpoint entity can be obtained automatically through projection. To guarantee that its projection is correct, i.e. it has the same behaviors of the original choreography, a choreography usually has to respect some coherency conditions. This restricts the set of choreographies that can be projected. In this paper, we present a transformation for amending choreographies that do not respect common syntactic conditions for projection correctness. Specifically, our transformation automatically reduces the amount of concurrency, and it infers and adds hidden communications that make the resulting choreography respect the desired conditions, while preserving its behavior.
Additional notes
Cite (BibTeX)
Click to expand
  author       = {Ivan Lanese and
                  Fabrizio Montesi and
                  Gianluigi Zavattaro},
  editor       = {Ant{\'{o}}nio Ravara and
                  Josep Silva},
  title        = {Amending Choreographies},
  booktitle    = {Proceedings 9th International Workshop on Automated Specification
                  and Verification of Web Systems, {WWV} 2013, Florence, Italy, 6th
                  June 2013},
  series       = {{EPTCS}},
  volume       = {123},
  pages        = {34--48},
  year         = {2013},
  url          = {},
  doi          = {10.4204/EPTCS.123.5},
  timestamp    = {Wed, 12 Sep 2018 01:05:16 +0200},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}

A PDF is available (possibly a preprint):

Download PDF