论文标题
通用多党会话类型带有崩溃失败（技术报告）
Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report)
论文作者
论文摘要
会话类型可以实现通信系统的规范和验证。但是，他们的理论通常认为过程永远不会失败。为了解决此限制，我们提出了一个具有崩溃失败的广义多党会话类型（MPST）理论，过程可以任意崩溃。 我们的新理论验证了更多的协议和流程W.R.T.以前的工作。我们将最小的句法更改应用于标准会话π-calculus和类型：我们在语义上进行崩溃及其处理，并在行为安全性属性上使用广义MPST键入系统参数。我们通过可选的可靠性假设涵盖了完全可靠的和完全不可靠的会话之间的频谱，并在存在崩溃停止故障的情况下证明了类型的安全性和协议一致性。 引入崩溃停止故障会带来非平凡的后果：编写正确的过程来处理所有崩溃方案可能很困难。但是，我们广义的MPST理论使我们能够通过模型检查驯服这种复杂性，以验证多方会话是否满足所需的行为属性，例如即使在出现坠机的情况下，僵尸也是僵局。我们使用MCRL2模型检查器实施我们的方法，并通过从文献中扩展的示例对其进行评估。
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.
