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.