Multiparty session nets

Abstract

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.