Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2022
|
| Sujets: | |
| Accès en ligne: | https://arxiv.org/abs/2204.07728 |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914676161380352 |
|---|---|
| author | Peters, Kirstin Nestmann, Uwe Wagner, Christoph |
| author_facet | Peters, Kirstin Nestmann, Uwe Wagner, Christoph |
| contents | Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance. We extend multiparty session types to cope with system failures such as unreliable communication and process crashes. Moreover, we augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors). To illustrate our approach we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2204_07728 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | FTMPST: Fault-Tolerant Multiparty Session Types Peters, Kirstin Nestmann, Uwe Wagner, Christoph Logic in Computer Science Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance. We extend multiparty session types to cope with system failures such as unreliable communication and process crashes. Moreover, we augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors). To illustrate our approach we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg. |
| title | FTMPST: Fault-Tolerant Multiparty Session Types |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2204.07728 |