Multiparty Session Nets
Multiparty Session Nets
复制标题
多方会话网络
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
N. Yoshida
中科院分区：
文献类型：
--
作者：
L. Fossati;Raymond Hu;N. Yoshida
本文提出了一种基于角色的编排规范来验证分布式多方系统的全局会话网，它是多方会话类型(MPST)和Petri网的结合。与标准的语法MPST相比，会话网的图形表示允许更自由地组合分支、合并、分叉和连接模式。我们使用会话网令牌动态来验证图形全局网和语法端点类型之间的灵活一致性，并应用该一致性来确保具有通道移动性的端点进程的类型安全和进度。我们已经实现了用于验证全局会话图的格式良好性和端点类型一致性的Java API。
This paper introduces global session nets, an integration of multiparty session types (MPST) and Petri nets, for role-based choreographic specifications to verify distributed multiparty systems. The graphical representation of session nets enables more liberal combinations of branch, merge, fork and join patterns than the standard syntactic MPST. We use session net token dynamics to verify a flexible conformance between the graphical global net and syntactic endpoint types, and apply the conformance to ensure type-safety and progress of endpoint processes with channel mobility. We have implemented Java APIs for validating global session graph well-formedness and endpoint type conformance.