CSP||B

A combined approach to specification development

  • General Tools

The philosophy of CSP||B is to make use of existing industrial strength tools. The main focus of verification is achieved via model checking

  • ProB is used to simulate and model check CSP||B descriptions. Using this tool it is also possible to check LTL and CTL properties of CSP||B descriptions.
  • FDR is a CSP tool to analyse the CSP descriptions.
We have also been developing a proof framework in the theorem prover PVS to support the verification of CSP||B specifications.