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.

翻译：多参与方会话类型旨在抽象地刻画通信协议的结构并验证行为属性。其中一项重要的属性是进展性，即无死锁特性。分布式算法通常类似于多参与方通信协议，但证明其属性（尤其是与进展性密切相关的终止性）可能相当复杂。由于分布式算法常被设计为应对故障，将容错机制融入会话类型是使用该技术验证分布式算法的首要步骤。我们扩展了多参与方会话类型以应对系统故障，例如不可靠通信和进程崩溃。此外，我们通过故障模式增强了进程语义，这些模式可用于表示系统需求（例如故障检测器）。为阐明我们的方法，本文对Chandra与Toueg提出的著名轮转协调算法的一个变体进行了分析。