License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.8.2.21
URN: urn:nbn:de:0030-drops-162196
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16219/
Go back to Dagstuhl Artifacts Series


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

Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)

pdf-format:
DARTS-8-2-21.pdf (0.7 MB)
artifact-format:
DARTS-8-2-21-artifact-bba5020e0c944a55be6951d8cba2acc3.zip (884 MB)

Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy.


Abstract

We introduce CAScr, the first implementation of Scribble (http://www.scribble.org, https://nuscr.dev/) that relies on choreography automata, for deadlock-free distributed programming. CAScr supports the main theoretical results and constructions in the related article. CAScr takes the popular top-down approach to system development, based on choreographic models, following the original methodology of Scribble and multiparty session types. The top-down approach enables correctness-by-construction: a developer provides a global description for the whole communication protocol; by projecting the global protocol, APIs are generated from local CFSMs, which ensure the safe implementation of each participant. The theory of choreography automata in the related article guarantees deadlock freedom for the distributed implementation of flexible global protocols. We target web development, supporting in particular the TypeScript programming language.

BibTeX - Entry

@Article{gheri_et_al:DARTS.8.2.21,
  author =	{Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
  title =	{{Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)}},
  pages =	{21:1--21:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16219},
  URN =		{urn:nbn:de:0030-drops-162196},
  doi =		{10.4230/DARTS.8.2.21},
  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: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)
Issue Date: 2022
Date of publication: 23.06.2022


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