License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2022.8
URN: urn:nbn:de:0030-drops-162367
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16236/
Go to the corresponding LIPIcs Volume Portal

Gheri, Lorenzo ; Lanese, Ivan ; Sayers, Neil ; Tuosto, Emilio ; Yoshida, Nobuko

Design-By-Contract for Flexible Multiparty Session Protocols

pdf-format:
LIPIcs-ECOOP-2022-8.pdf (1 MB)

Abstract

Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.

BibTeX - Entry

@InProceedings{gheri_et_al:LIPIcs.ECOOP.2022.8,
  author =	{Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
  title =	{{Design-By-Contract for Flexible Multiparty Session Protocols}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{8:1--8:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16236},
  URN =		{urn:nbn:de:0030-drops-162367},
  doi =		{10.4230/LIPIcs.ECOOP.2022.8},
  annote =	{Keywords: Choreography automata, design by contract, deadlock freedom, Communicating Finite State Machines, TypeScript programming}
}

Keywords: Choreography automata, design by contract, deadlock freedom, Communicating Finite State Machines, TypeScript programming
Collection: 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Issue Date: 2022
Date of publication: 23.06.2022
Supplementary Material: Software (ECOOP 2022 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.8.2.21
Software (Source Code): https://github.com/Tooni/CAScript-Artifact

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI