Existing industrial strength tools can readily be used to support the analysis of CSP||B specifications.

Currently researchers using CSP||B use the BToolkit and ProB to analyse the B method descriptions and FDR to analyse the CSP descriptions. Both are commercial tools.

We have also been developing a proof framework in the theorem prover PVS to support the verification of CSP||B specifications..

Investigations have been carried out in order to examine the potential of linking the B-Toolkit and ProBE. Please contact Helen Treharne for further information.