Multiparty Session Nets

Luca Fossati, Raymond Hu, Nobuko Yoshida

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

    5 Citations (Scopus)

    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.
    Original languageEnglish
    Title of host publicationTrustworthy Global Computing
    EditorsMatteo Maffei, Emilio Tuosto
    PublisherSpringer Nature
    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 Sept 20146 Sept 2014

    Publication series

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

    Conference

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

    Fingerprint

    Dive into the research topics of 'Multiparty Session Nets'. Together they form a unique fingerprint.

    Cite this