Skip to Main content Skip to Navigation
Conference papers

Typechecking Java Protocols with [St]Mungo

Abstract : This is a tutorial paper on [St]Mungo, a toolchain based on multiparty session types and their connection to typestates for safe distributed programming in Java language.The StMungo (“Scribble-to-Mungo”) tool is a bridge between multiparty session types and typestates. StMungo translates a communication protocol, namely a sequence of sends and receives of messages, given as a multiparty session type in the Scribble language, into a typestate specification and a Java API skeleton. The generated API skeleton is then further extended with the necessary logic, and finally typechecked by Mungo. The Mungo tool extends Java with (optional) typestate specifications. A typestate is a state machine specifying a Java object protocol, namely the permitted sequence of method calls of that object. Mungo statically typechecks that method calls follow the object’s protocol, as defined by its typestate specification. Finally, if no errors are reported, the code is compiled with javac and run as standard Java code.In this tutorial paper we give an overview of the stages of the [St]Mungo toolchain, starting from Scribble communication protocols, translating to Java classes with typestates, and finally to typechecking method calls with Mungo. We illustrate the [St]Mungo toolchain via a real-world case study, the HTTP client-server request-response protocol over TCP. During the tutorial session, we will apply [St]Mungo to a range of examples having increasing complexity, with HTTP being one of them.
Complete list of metadata

https://hal.inria.fr/hal-03283241
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, July 9, 2021 - 5:54:04 PM
Last modification on : Friday, July 9, 2021 - 5:57:24 PM
Long-term archiving on: : Sunday, October 10, 2021 - 8:29:19 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

A. Laura Voinea, Ornela Dardha, Simon J. Gay. Typechecking Java Protocols with [St]Mungo. 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2020, Valletta, Malta. pp.208-224, ⟨10.1007/978-3-030-50086-3_12⟩. ⟨hal-03283241⟩

Share

Metrics

Record views

33