Search 

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 ( 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 ( 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. ( 2005-08-28)
• here is a quick patch to correct a bug in distinction handling. Apply it and recompile. ( 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 compressed Postscript format for version 3.122.