The Mobility Workbench: A Tool for the Pi-Calculus

Björn Victor and Faron Moller

Abstract: 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.

Extract from the user's manual: The Mobility Workbench (MWB) is a tool for manipulating and analyzing mobile concurrent systems described in the pi-calculus, developed by Faron Moller and Björn Victor, in collaboration with Davide Sangiorgi at the University of Edinburgh. It is written in Standard ML, and currently runs under the New Jersey SML compiler.

In the current prototype version, the basic functionality is to decide the open bisimulation equivalences of Sangiorgi, for agents in the monadic pi-calculus with the original positive match operator. This is decidable for pi-calculus agents with finite control, correlating to CCS finite-state agents, which do not admit parallel composition within recursively defined agents.

The algorithm is based on the efficient characterization of the equivalence described in [Sangiorgi 1993], and (necessarily) generates the state space ``on the fly''. Versions for both the strong and weak equivalences are implemented. There are also commands e.g. for finding deadlocks and interactively simulating an agent.

The MWB is undergoing constant and dynamic changes. This guide describes the prototype version, but we are currently developing a new version with efficiency in focus, which supports the polyadic calculus, handles sorts, and has model checking commands.

LFCS report ECS-LFCS-94-285, February 1994.

Previous | Index | Next