Typechecking Protocols with Mungo and StMungo

Dimitrios Kouzapas, Ornela Dardha, Roly Perera, Simon J. Gay

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

Abstract

We report on two tools which extend Java with support for static typechecking of communication protocols. Our Mungo tool extends Java with typestate definitions, which allow classes to be associated with state machines defining permitted sequences of method calls. A complementary tool, StMungo, takes a communication protocol specified in the Scribble protocol description language, and generates a typestate specification for each endpoint, capturing the permitted sequences of messages along that channel. Endpoint implementations can be validated by Mungo against their typestate definitions and then compiled as usual with javac. We formalise Mungo’s typestate inference system and demonstrate the Scribble, Mungo and StMungo toolchain via a typechecked SMTP client that can communicate with a real-world SMTP server.
Original languageEnglish
Title of host publication18th International Symposium on Principles and Practice of Declarative Programming PPDP 2016
Place of PublicationEdinburgh, United Kingdom
PublisherACM
Pages146-159
Number of pages19
ISBN (Electronic)978-1-4503-4148-6
DOIs
Publication statusPublished - 5 Sep 2016
Event18th International Symposium on Principles and Practice of Declarative Programming - Edinburgh, United Kingdom
Duration: 5 Sep 20167 Sep 2016
http://ppdp16.webs.upv.es/

Conference

Conference18th International Symposium on Principles and Practice of Declarative Programming
Abbreviated titlePPDP 2016
CountryUnited Kingdom
CityEdinburgh
Period5/09/167/09/16
Internet address

Fingerprint Dive into the research topics of 'Typechecking Protocols with Mungo and StMungo'. Together they form a unique fingerprint.

Cite this