Tools for CSP

The emergence of tools for CSP has had a profound impact on the utility of the notation. These play a part in illustrating small systems for teaching purposes and analyzing industrial-size problems which would have been intractable using pencil and paper.This page lists some of the known tools for CSP, along with contact details where available.

Note that tools do not provide an alternative to understanding the theory of CSP: only those with a good grounding in the theory will be able to make truly effective use of them. The book is designed to provide just such a grounding.

The existence of tools has influenced the choice and presentation of the material in the book, however, and many of the examples and exercises were designed to exploit the capabilities of FDR.

FDR

FDR was the first commercially available tool for CSP and played a major role in driving the evolution of CSP from a blackboard notation to a concrete language. It allows the checking of a wide range of correctness conditions, including deadlock and livelock freedom as well as general safety and liveness properties. When these conditions are not satisfied, the reasons can be investigated.

FDR is a product of Formal Systems.

Though for general use this software needs a licence, it is configured to run the examples files from the book without this requirement and can be downloaded for a number of platforms via FTP.

ProBE

ProBE is another offering from Formal Systems. In contrast to FDR's automatic checking of properties, ProBE addresses the equally important need of the user to gain understanding of a system by interacting with it. This makes it an ideal companion to the book for those meeting CSP for the first time.

The user controls the resolution of non-determinism and the choice of actions, watching the process evolve in response. Component processes can be selected, and their contribution to the larger system examined.

More information, including the manual for ProBE, is available online. Demonstration copies, including the examples from the book, are available for download.

Deadlock Checker

The rules for deadlock freedom from chapter 13 (together with some other methods) have been implemented by Jeremy Martin as part of his doctoral research. This currently uses components from an early version of FDR to generate its network descriptions, and so uses a restricted dialect of the language, but this situation is under review. Details are available from his pages.

Casper

Casper is Gavin Lowe's security-protocol compiler (into CSP), discussed in chapter 15.

Other tools

Details of further tools will be added here later. If you either have, or know of, a tool that meets the criterion of being applicable to (or uses it in some other way, like Casper) the process algebra style of CSP (though there is no requirement that it should use exactly the same machine-readable language), and you would like a reference to it included on this page then please let the author know, giving him necessary details.