Typechecking Java Protocols with [St]Mungo - Formal Techniques for Distributed Objects, Components, and Systems
Conference Papers Year : 2020

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.
Fichier principal
Vignette du fichier
495615_1_En_12_Chapter.pdf (351.07 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-03283241 , version 1 (09-07-2021)

Licence

Identifiers

Cite

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⟩
66 View
31 Download

Altmetric

Share

More