We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, that is the sufficient conditions that guarantee a protocol to be implementable. We introduce a typing discipline that enforces well-formedness of typed choreographies. Then we unveil the relation among refinable choregraphies and their admissible refinements in terms of an axiom scheme.

Towards Refinable Choreographies

Ugo de'Liguoro;Hernán Melgratti;
2020-01-01

Abstract

We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, that is the sufficient conditions that guarantee a protocol to be implementable. We introduce a typing discipline that enforces well-formedness of typed choreographies. Then we unveil the relation among refinable choregraphies and their admissible refinements in terms of an axiom scheme.
2020
ICE 2020 - 13th Interaction and Concurrency Experience
Virtuale (originariamente Malta)
19-20 Giugno 2020
324
61
77
http://arxiv.org/abs/2009.07991v1
Computer Science - Logic in Computer Science; Computer Science - Logic in Computer Science; Computer Science - Software Engineering; D.1.3; D.2.4; D.3.1; F.3.1
Ugo de'Liguoro; Hernán Melgratti; Emilio Tuosto
File in questo prodotto:
File Dimensione Formato  
2020 dL Melgratti Tuosto - Towards Refinable Choreographies.pdf

Accesso aperto

Descrizione: Articolo principale
Tipo di file: PDF EDITORIALE
Dimensione 217.26 kB
Formato Adobe PDF
217.26 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1759629
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 0
social impact