The Paths to Choreography Extraction

Luís Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi [2016].
In CoRR abs/1610.10050.

Abstract

Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification (e.g., Multiparty Session Types) and synthesis of correct-by-construction software (Choreographic Programming). They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most existing software does not come with choreographies yet, which prevents their application. To attack this problem, we propose a novel methodology (called choreography extraction) that, given a set of programs or protocol specifications, automatically constructs a choreography that describes their behavior. The key to our extraction is identifying a set of paths in a graph that represents the symbolic execution of the programs of interest. Our method improves on previous work in several directions: we can now deal with programs that are equipped with a state and internal computation capabilities; time complexity is dramatically better; we capture programs that are correct but not necessarily synchronizable, i.e., they work because they exploit asynchronous communication.

Links

arxiv.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/Cruz-FilipeLM16,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Kim S. Larsen and
                  Fabrizio Montesi},
  title        = {The Paths to Choreography Extraction},
  journal      = {CoRR},
  volume       = {abs/1610.10050},
  year         = {2016},
  url          = {http://arxiv.org/abs/1610.10050},
  eprinttype    = {arXiv},
  eprint       = {1610.10050},
  timestamp    = {Mon, 13 Aug 2018 16:47:44 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/Cruz-FilipeLM16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Peer-reviewed version

Click to show in publication list