Generalised multiparty session types with crash-stop failures
Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily....
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2022
|
| _version_ | 1797111914691559424 |
|---|---|
| author | Barwell, AD Scalas, A Yoshida, N Zhou, F |
| author_facet | Barwell, AD Scalas, A Yoshida, N Zhou, F |
| author_sort | Barwell, AD |
| collection | OXFORD |
| description | Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checking, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature. |
| first_indexed | 2024-03-07T08:17:04Z |
| format | Conference item |
| id | oxford-uuid:57109ec0-8c9e-4c77-9664-e03407c4bf90 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:17:04Z |
| publishDate | 2022 |
| publisher | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| record_format | dspace |
| spelling | oxford-uuid:57109ec0-8c9e-4c77-9664-e03407c4bf902024-01-10T15:04:43ZGeneralised multiparty session types with crash-stop failuresConference itemhttp://purl.org/coar/resource_type/c_5794uuid:57109ec0-8c9e-4c77-9664-e03407c4bf90EnglishSymplectic ElementsSchloss Dagstuhl – Leibniz-Zentrum für Informatik2022Barwell, ADScalas, AYoshida, NZhou, FSession types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checking, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature. |
| spellingShingle | Barwell, AD Scalas, A Yoshida, N Zhou, F Generalised multiparty session types with crash-stop failures |
| title | Generalised multiparty session types with crash-stop failures |
| title_full | Generalised multiparty session types with crash-stop failures |
| title_fullStr | Generalised multiparty session types with crash-stop failures |
| title_full_unstemmed | Generalised multiparty session types with crash-stop failures |
| title_short | Generalised multiparty session types with crash-stop failures |
| title_sort | generalised multiparty session types with crash stop failures |
| work_keys_str_mv | AT barwellad generalisedmultipartysessiontypeswithcrashstopfailures AT scalasa generalisedmultipartysessiontypeswithcrashstopfailures AT yoshidan generalisedmultipartysessiontypeswithcrashstopfailures AT zhouf generalisedmultipartysessiontypeswithcrashstopfailures |