Fault-Tolerant Multiparty Session Types
Fault-Tolerant Multiparty Session Types
复制标题
容错多方会话类型
DOI：
10.46298/lmcs-19(4:14)2023
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Christopher Wagner
中科院分区：
文献类型：
--
作者：
Kirstin Peters;U. Nestmann;Christopher Wagner
多方会话类型旨在抽象地捕获
通信协议和验证行为属性。其中一个重要的
财产是进步，即，没有僵局。分布式算法
通常类似于多方通信协议。但证明他们的
属性，特别是与进度密切相关的终止，可以
要详细。由于分布式算法通常被设计为处理
故障，使用会话类型验证分布式
算法是集成容错。我们扩展了多方会话类型
以应对系统故障，如不可靠的通信和处理
崩溃了。此外，我们还通过故障模式来增强流程的语义
可用于表示系统要求（例如，失败
探测器）。为了说明我们的方法，我们分析了一个众所周知的变体，
Chandra和Toueg的旋转坐标算法。
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.
链路失败的会话类型
DOI：
10.1007/978-3-319-60225-7_1
发表时间：
2017
期刊：
影响因子：
--
作者：
Manuel Adameit;Kirstin Peters;Uwe Nestmann
通讯作者：
Uwe Nestmann