A SPATIAL LOGIC MODEL CHECKER

The introduction of dynamic spatial logics has been motivated by the recent shift of focus from monolithic concurrent systems towards distributed systems. Dynamic spatial logics support not just the specification of behavioral properties, but also of structural properties of concurrent systems, in a fairly integrated way. Many interesting properties of distributed systems are inherently spatial. Simple examples include: connectivity, stating that there is always an access route between two different sites, unique handling, stating that there is at most one server process listening on a given channel, resource availability, stating that a bound exists on the number of channels that can be allocated in a given location, or race freedom, stating that no competing requests will ever arise for the same service. Even secrecy can also be sometimes understood in spatial terms, since a secret is a piece of data whose knowledge of is restricted to some parts of a system, and unforgeable by other parts.

Prominent examples of spatial logics for distributed systems are currently the pi-calculus logics of Caires and Cardelli, the Ambient Logic of Cardelli and Gordon, and the decidable behavioral-spatial logic adressed by the Spatial Logic Model Checker; we provide a short bibliography about the development of dynamic spatial logics by several authors.

Our Spatial Logic Model Checker is a tool that allows the user to automatically verify behavioral and spatial properties of distributed concurrent systems expressed in the pi-calculus of Milner, Parrow and Walker. The algorithm implemented (currently using on-the-fly model-checking techniques) is provably correct for all processes, and complete for the class of bounded processes, an abstract class of processes that includes the finite control fragment of the pi-calculus.

The tool itself is written in OCaml, and runs on any platform supported by the OCaml distribution. It was implemented by Hugo Vieira, with a helping hand by Ruben Viegas in version 1.0, and developed by Hugo Vieira and Luís Caires.

This work has been mainly supported by the EU project FET IST-2001-33100 PROFUNDIS of the Global Computing Initiative. The tool (v0.91) is available online in the Profundis Web tool suite, thanks to a colaboration with the Pisa Profundis team.

The current distribution consists of a single executable, available in OCaml bytecode and native code for both Microsoft Windows and Mac OS X, the source code, a preliminary user's manual, and a few examples along with their descriptions.