The readers/writers problem describes a protocol for coordination of N readers and N writers accessing a shared resource.
The CSP definition of Readers-Writers Problem of size N is defined as follows.
The property to verify is reachability of an erroneous situation (i.e., wrong readers/writers coordination).
The following defintion is the MS example with size 2.
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.
CSP simulator takes in the specifications and allows users to perform various simulation tasks:
- Complete states generation based on the execution graph. The generation may not terminate if the states are not finite.
- Automatically Random Simulation with animation
- User interactive simulation with Step by Step execution
- Trace display and replay
Specification editor accepts the CSP specifications and LTL properties defined in How to write Process Definitions and How to write LTL Formulae respectively.
Specification editor has an extremely user friendly user interface with following features:
- Complete text editing functions
- Syntax highlighting
- Multi-threading execution
- Multi-documents environment