Applied Choreographies

Maurizio Gabbrielli, Saverio Giallorenzo, Fabrizio Montesi [2015].
In CoRR abs/1510.03637.

Abstract

Choreographic Programming is a correct-by-construction paradigm where a compilation procedure synthesises deadlock-free, concurrent, and distributed communicating processes from global, declarative descriptions of communications, called choreographies. Previous work used choreographies for the synthesis of programs. Alas, there is no formalisation that provides a chain of correctness from choreographies to their implementations. This problem originates from the gap between existing theoretical models, which abstract communications using channel names (\`a la CCS/{\pi}-calculus), and their implementations, which use low-level mechanisms for message routing. As a solution, we propose the theoretical framework of Applied Choreographies. In the framework, developers write choreographies in a language that follows the standard syntax and name-based communication semantics of previous works. Then, they use a compilation procedure to transform a choreography into a low-level, implementation-adherent calculus of Service-Oriented Computing (SOC). To manage the complexity of the compilation, we divide its formalisation and proof in three stages, respectively dealing with: a) the translation of name-based communications into their SOC equivalents (namely, using correlation mechanisms based on message data); b) the projection of a choreography into a composition of partial, single-participant choreographies (towards their translation into SOC processes); c) the translation of partial choreographies and the distribution of choreography-level state into SOC processes. We provide results of behavioural correspondence for each stage. Thus, given a choreography specification, we guarantee to synthesise its faithful and deadlock-free service-oriented implementation.

Links

arxiv.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/GabbrielliGM15,
  author       = {Maurizio Gabbrielli and
                  Saverio Giallorenzo and
                  Fabrizio Montesi},
  title        = {Applied Choreographies},
  journal      = {CoRR},
  volume       = {abs/1510.03637},
  year         = {2015},
  url          = {http://arxiv.org/abs/1510.03637},
  eprinttype    = {arXiv},
  eprint       = {1510.03637},
  timestamp    = {Mon, 13 Aug 2018 16:48:53 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/GabbrielliGM15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Peer-reviewed version

Click to show in publication list

A PDF is available (possibly a preprint):