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