logo Mungo

Mungo

Mungo is a Java front-end tool used to statically check the order of method calls. It is implemented using the JastAdd framework. A protocol definition is described as a sequence of method calls, the order of which determines the validity of the protocol.

A typestate file is defined and associated to a class. The Mungo tool checks that the object instantiating the class performs method calls by following its declared typestate. If the object respects the typestate, then .java files are produced, for every .mungo file in the program. Finally, the Java tools can be used to compile and run the standard Java code. If the typestate is violated, Mungo reports the errors.

The Mungo tool is devoloped and maintained by Dr. Dimitrios Kouzapas.

Source on Bitbucket

StMungo

StMungo (Scribble to Mungo) is a Java-based tool used to translate Scribble local protocol specifications into typestate specifications. It is implemented using the ANTLR v4.5 framework. After the translation, we use Mungo to statically typecheck the protocol implementation.

We start from a distributed multiparty protocol defined as Scribble global protocol and then use the Scribble tools to validate and project into a local protocol describing the interactions from the point of view of one participant. For every participant, there is a local projection.

For every Scribble local protocol, StMungo produces .mungo files containing: a typestate specification decribing the local protocol as a sequence of method calls, an API for the participant implementing the methods in the typestate and a main() method skeleton calling the methods in the typestate.

The StMungo tool is developed and maintained by Dr. Ornela Dardha.

Source on Bitbucket