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系统。