A SPATIAL LOGIC MODEL CHECKER

for Concurrency, Distribution and Mobility


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.

Distribution
(v2.01-Nov-09)

Mac OS X 10.5
(requires OCaml runtime v3.10)

Mac OS X 10.5 native
(runs standalone)

Microsoft Windows
(requires OCaml runtime v3.08)

Microsoft Windows native
(runs standalone)

Source code

(license)

(change log)

Some simple examples

gossip
ring
phones
arrow
choreography
(info)
(info)
(info)
(info)
(info)

Papers

  • Luís Caires, Behavioral and Spatial Observations in a Logic for the Pi-Calculus, FoSSaCS 2004, ETAPS 2004, Barcelona, 2004. (ps)

  • Hugo Vieira and Luís Caires, The Spatial Logic Model Checker User's Manual v1.15. (pdf)

  • Bernardo Toninho and Luís Caires, A Spatial-Epistemic Logic for Reasoning About Security Protocols, SecCo 2010. (pdf)

  • Luís Caires and Hugo Torres Vieira, SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications, to appear in TACAS 2012. (pdf)

See also:

Extensions

Model Checking Security Protocols

SLMC-K is an extension of SLMC intended for security protocol verification. The modelling language is a variant of the applied pi-calculus of Abadi and Fournet, while specifications are expressed in a dynamic spatial logic extended with an epistemic operator that talks about process knowledge. The theory behind SLMC-K is described in the paper "A Spatial-Epistemic Logic and Tool for Reasoning about Security Protocols" (see above).

Model Checking the Conversation Calculus

Version 2.01 supports the specification of systems using the Conversation Calculus, a model for dynamic multiparty service-oriented applications introduced by Vieira, Caires and Seco. This extension to the tool allows to model-check Conversation Calculus specifications against dynamic spatial logic properties. The development of this extension of the tool was supported by IP Sensoria (EU IST FP6) and is reported in the Tools and Verification chapter of the Sensoria book.

Related links

Web page and software maintained by: di.fc.ul.pt, htv@; di.fct.unl.pt, luis.caires@