In this paper we describe the first prototype version of the Mobility Workbench (MWB), an automated tool for manipulating and analyzing mobile concurrent systems (those with evolving connectivity structures) described in the pi-calculus. The main feature of this version of the MWB is checking open bisimulation equivalences. We illustrate the MWB with an example automated analysis of a handover protocol for a mobile telephone system.
CAV'94 version, March 1994 (Postscript version, compressed)
DoCS Technical report 94/45, February 1994 (Postscript version, compressed)
(Also available as LFCS report ECS-LFCS-94-285)
MWB Web page
MWB distribution directory
@InProceedings{vm:mwb,
author = "Bj{\"o}rn Victor and Faron Moller",
title = "The {M}obility {W}orkbench --- A Tool for the $\pi$-Calculus",
editor = "David Dill",
volume = "818",
series = "Lecture Notes in Computer Science",
pages = "428-440",
booktitle = "CAV'94: Computer Aided Verification",
year = "1994",
publisher = "Springer-Verlag"
}
@TechReport{vm:mwb:rep,
author = "Bj{\"o}rn Victor and Faron Moller",
title = "The {M}obility {W}orkbench --- A Tool for the $\pi$-Calculus",
institution = "Department of Computer Systems, Uppsala University, Sweden",
year = 1994,
number = "DoCS 94/45",
month = "February",
note = "Also available as Technical Report ECS-LFCS-94-285,
Laboratory for Foundations of Computer Science,
Department of Computer Science, University of Edinburgh, UK"
}