FTMPST：容错多方会话类型
摘要：使用多方会话类型来抽象地捕捉通信协议的结构并验证行为属性。其中一个重要属性是进展，即死锁的缺失。分布式算法经常类似于多方通信协议。但是证明它们的属性，特别是与进展密切相关的终止性，可能会很复杂。由于分布式算法通常设计用于处理故障，使用会话类型验证分布式算法的第一步是集成容错能力。我们扩展了多方会话类型以处理系统故障，例如不可靠的通信和进程崩溃。此外，我们通过故障模式来增加过程的语义，可以用来表示系统要求（例如故障检测器）。为了说明我们的方法，我们分析了Chandra和Toueg的著名旋转协调器算法的变体。
作者：Kirstin Peters and Uwe Nestmann and Christoph Wagner
论文ID：2204.07728
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-29