Implementing Choreography Extraction

Luís Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi, Larisa Safina [2022].
In CoRR abs/2205.02636.

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 behaviour 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 and time complexity is dramatically better. We also implement this theory and show that, in spite of its theoretical exponential complexity, it is usable in practice. We discuss the data structures needed for an efficient implementation, introduce some optimisations, and perform a systematic practical evaluation.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/abs-2205-02636,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Kim S. Larsen and
                  Fabrizio Montesi and
                  Larisa Safina},
  title        = {Implementing Choreography Extraction},
  journal      = {CoRR},
  volume       = {abs/2205.02636},
  year         = {2022},
  url          = {https://doi.org/10.48550/arXiv.2205.02636},
  doi          = {10.48550/ARXIV.2205.02636},
  eprinttype    = {arXiv},
  eprint       = {2205.02636},
  timestamp    = {Wed, 11 May 2022 17:29:40 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2205-02636.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}