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 {\pi}-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.

翻译：会话类型能够对通信系统进行规约和验证。然而，其理论通常假设进程永远不会发生故障。为解决此局限，我们提出了一种支持崩溃停止故障的广义多方会话类型理论，其中进程可能任意崩溃。与先前工作相比，我们的新理论能够验证更多协议和进程。我们对标准会话π演算及其类型进行了最小语法修改：通过语义方式建模崩溃及其处理，并构建了一个参数化行为安全属性的广义多方会话类型系统。通过可选可靠性假设，我们涵盖了从完全可靠到完全不可靠会话的完整谱系，并证明了在崩溃停止故障存在下的类型安全性与协议一致性。引入崩溃停止故障会产生重要影响：编写能处理所有崩溃场景的正确进程十分困难。然而，我们的广义多方会话类型理论通过模型检验能够有效控制此复杂度，从而验证多方会话是否满足期望的行为属性（例如无死锁或活跃性），即使存在崩溃故障。我们使用mCRL2模型检验器实现了该方法，并通过文献延伸案例进行了评估。