具有崩溃停止故障的通用多方会话类型（技术报告）
Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report)
摘要：
会话类型支持通信系统的规范和验证。然而，他们的理论通常假设过程永远不会失败。为了解决这个问题，我们提出了一个广义多方会话类型（MPST）理论与崩溃停止故障，其中进程可以崩溃任意。我们的新理论验证了更多的协议和过程w.r.t.以前的工作。我们将最小的语法变化应用于标准会话π-演算和类型：我们对崩溃及其处理进行语义建模，并在行为安全属性上使用广义MPST类型系统参数。我们涵盖了完全可靠和完全不可靠的会话之间的频谱，通过可选的可靠性假设，并证明了类型安全性和协议一致性的崩溃停止故障的存在。引入崩溃停止失败会产生重要的后果：编写处理所有崩溃场景的正确进程可能很困难。然而，我们的广义MPST理论允许我们驯服这种复杂性，通过模型检验，以验证多方会话是否满足所需的行为属性，例如死锁自由或活性，即使在崩溃的存在。我们使用mCRL 2模型检查器实现我们的方法，并从文献中扩展的例子进行评估。
英文摘要：
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 π-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
