Hybrid Session Verification Through Endpoint API Generation

Raymond Hu, Nobuko Yoshida

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

    43 Citations (Scopus)


    This paper proposes a new hybrid session verification methodology for applying session types directly to mainstream languages, based on generating protocol-specific endpoint APIs from multiparty session types. The API generation promotes static type checking of the behavioural aspect of the source protocol by mapping the state space of an endpoint in the protocol to a family of channel types in the target language. This is supplemented by very light run-time checks in the generated API that enforce a linear usage discipline on instances of the channel types. The resulting hybrid verification guarantees the absence of protocol violation errors during the execution of the session. We implement our methodology for Java as an extension to the Scribble framework, and use it to specify and implement compliant clients and servers for real-world protocols such as HTTP and SMTP.
    Original languageEnglish
    Title of host publicationFundamental Approaches to Software Engineering
    PublisherSpringer Nature
    Number of pages18
    ISBN (Electronic)978-3-662-49665-7
    ISBN (Print)978-3-662-49664-0
    Publication statusPublished - 2 Apr 2016

    Publication series

    NameLecture Notes in Computer Science


    Dive into the research topics of 'Hybrid Session Verification Through Endpoint API Generation'. Together they form a unique fingerprint.

    Cite this