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.
翻译:会话类型允许对通信系统进行规格和核查。 但是,他们的理论常常假设, 程序永远不会失败。 为了解决这一限制, 我们提出了一个泛泛的多党会式(MPST) 理论, 其类型为崩溃停止失败, 程序可能会任意崩溃。 我们的新理论验证了更多的协议和程序 w.r.t. 以前的工作。 我们对标准会话 {pi} 计算和类型应用了最小的合成修改: 我们模拟碰撞及其处理的语义性, 在行为安全属性上有一个通用的 MPST 打字系统参数。 我们通过选择性的可靠性假设来覆盖完全可靠和完全不可靠的会话之间的频谱, 并证明在出现崩溃停止失败的情况下, 类型安全和协议符合。 引入崩溃停止失败会带来非三重后果: 正确处理所有崩溃情景的程序可能很困难 。 然而, 我们通用的MPST理论允许我们通过模式检查来适应这一复杂性, 以验证多党会会话是否满足预期的行为特性, 例如, 僵局自由或生活状况, 甚至在发生碰撞时, 我们使用 mCR2 模式校验, 评估从文献中扩展了它。