DARTS.8.2.21.pdf
- Filesize: 0.7 MB
- 5 pages
Document
Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)
Authors
Lorenzo Gheri 
,
Ivan Lanese ,
Neil Sayers ,
Emilio Tuosto ,
Nobuko Yoshida
-
Part of:
Issue:
Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Volume: DARTS, Volume 8 (ECOOP 2022)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-23
Artifact Description
Document Identifiers
Author Details
Acknowledgements
We thank the anonymous reviewers for their useful comments and suggestions. We thank Franco Barbanera for contributing to this work in its early stages. We thank Fangyi Zhou for their help with building our artifact on top of their software, νScr.
Cite AsGet BibTex
Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-by-Contract for Flexible Multiparty Session Protocols (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/DARTS.8.2.21
https://doi.org/10.4230/DARTS.8.2.21
Artifact
DARTS-8-2-21-artifact-bba5020e0c944a55be6951d8cba2acc3.zip
(Filesize: 0.86 GB)
Artifact 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.
Subject Classification
ACM Subject Classification
- Theory of computation → Distributed computing models
- Software and its engineering → Formal software verification
Keywords
- Choreography automata
- design by contract
- deadlock freedom
- Communicating Finite State Machines
- TypeScript programming
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-by-Contract for Flexible Multiparty Session Protocols. In 36th European Conference on Object-Oriented Programming (ECOOP 2022), 2022.
