We study the relationship between session types and behavioural contracts, representing Communicating Finite State Machines (CFSMs), under the assumption that processes communicate asynchronously. Session types represent a syntax-based approach for the description of communication protocols, while behavioural contracts, formally expressing CFSMs, follow an operational approach. We show the existence of a fully abstract interpretation of session types into a fragment of contracts that maps session subtyping into binary compliance-preserving CFSMs/behavioural contract refinement. In this way, on the one hand, we enrich the theory of session types with an operational characterization and, on the other hand, we use recent undecidability results for asynchronous session subtyping to obtain an original undecidability result for asynchronous CFSMs/behavioural contract refinement.

Asynchronous session subtyping as communicating automata refinement / Bravetti M.; Zavattaro G.. - In: SOFTWARE AND SYSTEMS MODELING. - ISSN 1619-1366. - ELETTRONICO. - 20:2(2021), pp. 311-333. [10.1007/s10270-020-00838-x]

Asynchronous session subtyping as communicating automata refinement

Bravetti M.;Zavattaro G.
2021

Abstract

We study the relationship between session types and behavioural contracts, representing Communicating Finite State Machines (CFSMs), under the assumption that processes communicate asynchronously. Session types represent a syntax-based approach for the description of communication protocols, while behavioural contracts, formally expressing CFSMs, follow an operational approach. We show the existence of a fully abstract interpretation of session types into a fragment of contracts that maps session subtyping into binary compliance-preserving CFSMs/behavioural contract refinement. In this way, on the one hand, we enrich the theory of session types with an operational characterization and, on the other hand, we use recent undecidability results for asynchronous session subtyping to obtain an original undecidability result for asynchronous CFSMs/behavioural contract refinement.
2021
Asynchronous session subtyping as communicating automata refinement / Bravetti M.; Zavattaro G.. - In: SOFTWARE AND SYSTEMS MODELING. - ISSN 1619-1366. - ELETTRONICO. - 20:2(2021), pp. 311-333. [10.1007/s10270-020-00838-x]
Bravetti M.; Zavattaro G.
File in questo prodotto:
File Dimensione Formato  
Bravetti-Zavattaro2021_Article_AsynchronousSessionSubtypingAs.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione 615.24 kB
Formato Adobe PDF
615.24 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/11585/819015
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 1
social impact