Skip to Main content Skip to Navigation
Journal articles

Asynchronous session subtyping as communicating automata refinement

Mario Bravetti 1, 2 Gianluigi Zavattaro 1, 2 
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-03340699
Contributor : Zavattaro Gianluigi Connect in order to contact the contributor
Submitted on : Friday, September 10, 2021 - 12:15:18 PM
Last modification on : Friday, July 8, 2022 - 10:08:21 AM

File

Bravetti-Zavattaro2021_Article...
Files produced by the author(s)

Identifiers

Collections

Citation

Mario Bravetti, Gianluigi Zavattaro. Asynchronous session subtyping as communicating automata refinement. Software and Systems Modeling, Springer Verlag, 2021, 20, pp.311 - 333. ⟨10.1007/s10270-020-00838-x⟩. ⟨hal-03340699⟩

Share

Metrics

Record views

7

Files downloads

21