The Paths to Choreography Extraction

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

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.
Additional notes
Cite (BibTeX)
Click to expand
  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          = {},
  eprinttype    = {arXiv},
  eprint       = {1610.10050},
  timestamp    = {Mon, 13 Aug 2018 16:47:44 +0200},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}

Peer-reviewed version
Click to show in publication list