Skip to main content
Department of Information Technology

The Mobility Workbench

The Mobility Workbench (MWB) is a tool for manipulating and analyzing mobile concurrent systems described in the pi-calculus. The tool has been developed by Björn Victor, Faron Moller, Mads Dam, and Lars-Henrik Eriksson.

MWB is written in Standard ML, and currently runs under the New Jersey SML compiler version 110. SML/NJ is currently available from http://smlnj.org.

The latest released version is MWB'99, which features a new faster model checker as well as decreased space requirements for open bisimilarity checking. It also supports checking hyperequivalence for the fusion calculus.

The MWB distribution directory is available by HTTP. There you can, e.g., find the sources of MWB'99 (updated.gif 2006-08-19), the user's guide for a previous version, and documentation for the new model checker.

There are also some brief installation instructions (updated.gif 2006-08-20). Note in particular the instructions for compiling in 110.0.7.

NOTE: the bug reporting address should now be !

NOTE: if you have a version of MWB'99 prior to 4.136,

  • here is a quick patch to make MWB compile in SML/NJ 110.55. Apply it to the mwb99 sources, and say sml -m sources.cm saveit.sml. (updated.gif 2005-08-28)
  • here is a quick patch to correct a bug in distinction handling. Apply it and recompile. (updated.gif 2006-08-19)

Those patches are already applied to the sources linked to above.

Papers:

Symbolic Characterizations and Algorithms for Hyperequivalence
by Björn Victor
describes the fusion calculus implementation and its theory.
A Verification Tool for the Polyadic Pi-Calculus
by Björn Victor
describes the polyadic version, and the weak open bisimulation equivalence.
The Mobility Workbench: A Tool for the Pi-Calculus
by Björn Victor and Faron Moller
describes the prototype monadic version.
The Mobility Workbench User's Guide
in PDF format and compressed Postscript format for version 3.122.
Updated  2016-08-17 15:26:35 by Björn Victor.