FDR
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)
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)