Design-by-contract for flexible multiparty session protocols
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...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2022
|
| _version_ | 1826311805157244928 |
|---|---|
| author | Gheri, L Lanese, I Sayers, N Tuosto, E Yoshida, N |
| author_facet | Gheri, L Lanese, I Sayers, N Tuosto, E Yoshida, N |
| author_sort | Gheri, L |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T08:16:40Z |
| format | Conference item |
| id | oxford-uuid:1a6b5c89-9d8e-43a3-acbe-4a3a8c619207 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:16:40Z |
| publishDate | 2022 |
| publisher | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| record_format | dspace |
| spelling | oxford-uuid:1a6b5c89-9d8e-43a3-acbe-4a3a8c6192072024-01-10T15:27:36ZDesign-by-contract for flexible multiparty session protocolsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:1a6b5c89-9d8e-43a3-acbe-4a3a8c619207EnglishSymplectic ElementsSchloss Dagstuhl – Leibniz-Zentrum für Informatik2022Gheri, LLanese, ISayers, NTuosto, EYoshida, NChoreographic 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. |
| spellingShingle | Gheri, L Lanese, I Sayers, N Tuosto, E Yoshida, N Design-by-contract for flexible multiparty session protocols |
| title | Design-by-contract for flexible multiparty session protocols |
| title_full | Design-by-contract for flexible multiparty session protocols |
| title_fullStr | Design-by-contract for flexible multiparty session protocols |
| title_full_unstemmed | Design-by-contract for flexible multiparty session protocols |
| title_short | Design-by-contract for flexible multiparty session protocols |
| title_sort | design by contract for flexible multiparty session protocols |
| work_keys_str_mv | AT gheril designbycontractforflexiblemultipartysessionprotocols AT lanesei designbycontractforflexiblemultipartysessionprotocols AT sayersn designbycontractforflexiblemultipartysessionprotocols AT tuostoe designbycontractforflexiblemultipartysessionprotocols AT yoshidan designbycontractforflexiblemultipartysessionprotocols |