The chief proof and analytic tool for CSP at present is called FDR
(standing
for Failures/Divergences Refinement). FDR is a model checking tool
which allows the verification 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.
Related publications
1. Formal Systems (Europe) Ltd., Failures-Divergences Refinement - FDR2
User Manual, 1999. (
PDF)
2. A. W. Roscoe, The theory and practice of concurrency (Appendix C -
The operation of FDR), Prentice Hall, 1998. (
PDF)
links
FDR download page
