University of Hertfordshire

By the same authors

Multiparty Session Nets

Research output: Chapter in Book/Report/Conference proceedingConference contribution

View graph of relations
Original languageEnglish
Title of host publicationTrustworthy Global Computing
EditorsMatteo Maffei, Emilio Tuosto
PublisherSpringer
Pages112-127
Number of pages25
ISBN (Electronic)978-3-662-45917-1
ISBN (Print) Print ISBN 978-3-662-45916-4
DOIs
Publication statusPublished - 23 Dec 2014
Event9th International Symposium, TGC 2014 - Rome, Italy
Duration: 5 Sep 20146 Sep 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8902
ISSN (Print)0302-9743

Conference

Conference9th International Symposium, TGC 2014
CountryItaly
CityRome
Period5/09/146/09/14

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.

Notes

© Springer-Verlag Berlin Heidelberg 2014.

ID: 17777667