Explicit Connection Actions in Multiparty Session Types

Raymond Hu, Nobuko Yoshida

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

    25 Citations (Scopus)

    Abstract

    This work extends asynchronous multiparty session types (MPST) with explicit connection actions to support protocols with optional and dynamic participants. The actions by which endpoints are connected and disconnected are a key element of real-world protocols that is not treated in existing MPST works. In addition, the use cases motivating explicit connections often require a more relaxed form of multiparty choice: these extensions do not satisfy the conservative restrictions used to ensure safety in standard syntactic MPST. Instead, we develop a modelling-based approach to validate MPST safety and progress for these enriched protocols. We present a toolchain implementation, for distributed programming based on our extended MPST in Java, and a core formalism, demonstrating the soundness of our approach. We discuss key implementation issues related to the proposed extensions: a practical treatment of choice subtyping for MPST progress, and multiparty correlation of dynamic binary connections.
    Original languageEnglish
    Title of host publicationFundamental Approaches to Software Engineering
    EditorsMarieke Huisman, Julia Rubin
    PublisherSpringer Nature Link
    Pages116-133
    Number of pages27
    ISBN (Electronic)978-3-662-54494-5
    ISBN (Print)978-3-662-54493-8
    DOIs
    Publication statusPublished - 22 Mar 2017
    EventInternational Conference on Fundamental Approaches to Software Engineering - Uppsala, Sweden
    Duration: 26 Apr 201728 Apr 2017

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume10202

    Conference

    ConferenceInternational Conference on Fundamental Approaches to Software Engineering
    Country/TerritorySweden
    CityUppsala
    Period26/04/1728/04/17

    Fingerprint

    Dive into the research topics of 'Explicit Connection Actions in Multiparty Session Types'. Together they form a unique fingerprint.

    Cite this