We have implemented both explicit model checking as well as bounded model checking for systematic analysis of CSP models. In our implementation, there is 2 model checkers are implemented:
- On-the-fly model checking: to verify the CSP processes with or without fair events.
- Bounded model checking: to verify the CSP processes without fair events based on the SAT Solvers.
The details of the two model checkers are in the submitted publications.