The Paths to Choreography Extraction

Luís Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi [2017].
In proceedings of FoSSaCS 2017, pp. 424-440.

Abstract

Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behavior of a given set of programs or protocol specifications.

We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation; time complexity is dramatically better; and we capture programs that work by exploiting asynchronous communication.

Links
doi.org
Additional notes
None
Cite (BibTeX)
Click to expand
@inproceedings{DBLP:conf/fossacs/Cruz-FilipeLM17,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Kim S. Larsen and
                  Fabrizio Montesi},
  editor       = {Javier Esparza and
                  Andrzej S. Murawski},
  title        = {The Paths to Choreography Extraction},
  booktitle    = {Foundations of Software Science and Computation Structures - 20th
                  International Conference, {FOSSACS} 2017, Held as Part of the European
                  Joint Conferences on Theory and Practice of Software, {ETAPS} 2017,
                  Uppsala, Sweden, April 22-29, 2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10203},
  pages        = {424--440},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-662-54458-7\_25},
  doi          = {10.1007/978-3-662-54458-7\_25},
  timestamp    = {Wed, 25 Sep 2019 18:04:52 +0200},
  biburl       = {https://dblp.org/rec/conf/fossacs/Cruz-FilipeLM17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):

Download PDF