PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

Model Checkers

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.