Multiparty session types (MPST) are a specification and verification framework for distributed message-passing systems. The communication protocol of the system is specified as a global type, from which a collection of local types (local process implementations) is obtained by endpoint projection. A global type is a single disciplining entity for the whole system, specified by one designer that has full knowledge of the communication protocol. On the other hand, distributed systems are often described in terms of their components: a different designer is in charge of providing a subprotocol for each component. The problem of modular specification of global protocols has been addressed in the literature, but the state of the art focuses only on dual input/output compatibility. Our work overcomes this limitation. We propose the first MPST theory of multiparty compositionality for distributed protocol specification that is semantics-preserving, allows the composition of two or more components, and retains full MPST expressiveness. We introduce hybrid types for describing subprotocols interacting with each other, define a novel compatibility relation, explicitly describe an algorithm for composing multiple subprotocols into a well-formed global type, and prove that compositionality preserves projection, thus retaining semantic guarantees, such as liveness and deadlock freedom. Finally, we test our work against real-world case studies and we smoothly extend our novel compatibility to MPST with delegation and explicit connections.

翻译：多参与方会话类型（MPST）是一种用于分布式消息传递系统的规范与验证框架。系统的通信协议被指定为全局类型，并通过端点投影从中获得一组局部类型（局部进程实现）。全局类型是整个系统的单一规约实体，由完全了解通信协议的设计者指定。另一方面，分布式系统通常根据其组件来描述：不同的设计者负责为每个组件提供子协议。全局协议的模块化规约问题已在文献中得到探讨，但现有研究仅关注双输入/输出兼容性。我们的工作克服了这一局限。我们提出了首个基于语义保持、支持两个或多个组件组合、并保留完整MPST表达能力的分布式协议规约的多参与方组合性MPST理论。我们引入用于描述子协议间交互的混合类型，定义了一种新的兼容性关系，明确描述了将多个子协议组合成良构全局类型的算法，并证明了组合性保持投影特性，从而保留活性与无死锁等语义保证。最后，我们通过实际案例验证了该方法，并将新型兼容性平滑扩展至支持委托与显式连接的MPST系统。