Book cover    CSP Tools

This page describes a number of tools which allow their users to animate, analyse and verify programs written in CSP.
An important issue is whether a given tool uses the CSPM version of machine-readable CSP or some other, custom version.  There are clear advantages to using a uniform syntax between tools.  The parser for CSPM, originally created by Bryan Scattergood and as used by FDR and ProBE, is freely available from Formal Systems or the author's group. A second parser which at the time of writing is nearly compliant with the CSPM syntax is under development by Michael Leuschel's group at Dusseldorf.

If you are the author of a CSP-based tool which you would like to be included in this page, please contact Bill Roscoe.

FDR (Failures Divergences Refinement) is the best-known CSP tool as is described at some length in UCS and TPC.  It is primarily a refinement checker for CSP's behavioural models such as traces and failures.  It only works on finite-state processes.  Details of its availability are here.

ProBE (Process Behaviour Explorer) is an animator for CSP based on the same CSPM compiler as FDR (though the present release is based on CSPM language of TPC, without the enhancements such as the throw operator [|A|> of UCS and FDR2.9X.  It allows you to explore the state space of (even infinite-state) CSP processes and search for certain types of state and actions.
It is freely available from here.

Checker is a prototype CSPM type checker.  It is not integrated with ProBE and FDR because its implementation, in attempting to be liberal in how to interpret the infix dot used in constructing events c.3 and data types, encountered much branching in its search for a type for a CSPM program.  This means that it can be very slow and produce very repetitive output on some programs.  It is a tool for the relatively experienced CSPM writer rather than the beginner.
CSPM would benefit from a less tolerant but faster type checker.

ProB is primarily a tool for analysing specifications cast in B (so it is pronounced "Pro B"), but allows integration of CSP and B and therefore also supports some analysis of CSP.  It aims to support CSPM but at the time of writing there are a few differences.  It provides an animation interface rather like ProBE as well as providing some model checking capability (LTL, deadlock, trace refinement).  It has a good integration of syntax and semantics.  It is more tolerant of processes with infinite and very large alphabets than FDR, and more tolerant of component processes with infinite and large state spaces.  At the time of writing its state exploration on most examples is very much slower than FDR.

ARC (Adelaide Refinement Checker) was developed as a CSP development/verification tools at the University of Adelaide.  It worked for a language which was CSPM without almost all of the functional programming.  It had an animator, type checker and refinement checker for CSP.  Of these the most interesting was the refinement checker, since it used the symbolic model checking technique of BDDs.  Unfortunately that is not included in the version presently downloadable from the web.

PAT is an ambitious model checking environment one of whose modes checks a rather liberal interpretation of CSP in ways that do not seem close to the semantics set out in UCS.  Its language includes shared variables in CSP.

CSP Prover is an integration of the theory of CSP with the theorem prover Isabelle.  Theorem proving is a very different technology from model checking.  Rather than automatically analysing the state spaces of finite state systems, it attempts to prove general results more as a traditional mathematician would based on the theory that has been loaded.
It is therefore better adapted to proving general results (such as algebraic laws) but not so good at the intensely combinatorial problems where FDR excels.


This site is presently under construction