MobilityReadingGroup

Multiparty Session Nets

Luca FOSSATI, Raymond HU, Nobuko YOSHIDA

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.

@inproceedings{FHY2014,
  author = {Luca Fossati and Raymond Hu and Nobuko Yoshida},
  title = {{Multiparty Session Nets}},
  booktitle = {9th International Symposium on Trustworthy Global Computing},
  series = {LNCS},
  volume = {8902},
  pages = {112--127},
  publisher = {Springer},
  year = 2014
}

@inproceedings{FHY2014,
  author = {Luca Fossati and Raymond Hu and Nobuko Yoshida},
  title = {{Multiparty Session Nets}},
  booktitle = {9th International Symposium on Trustworthy Global Computing},
  series = {LNCS},
  volume = {8902},
  pages = {112--127},
  publisher = {Springer},
  doi = "10.1007/978-3-662-45917-1_8",
  year = 2014
}