SyncStitch: A Model Checker based on the process algebra CSP
| Overview |
| System Requirements |
| Documentation |
| Download |
| Purchase |
| License Notice |
| FAQ |
| History |
Overview
SyncStitch is a model checker based on the process algebra CSP (Communicating Sequential Processes). By using SyncStitch, you can check six types of properties of the system you are developping:
- Deadlocks
- Divergences (also known as livelocks)
- Refinement relation on traces semantics (safety)
- Refinement relation on stable failures semantics (safety and liveness)
- LTL (Linear-Time Logic) with fluents and enabledness
- CTL (Computation-Tree Logic) with fluents and enabledness. In addition, three types of fairness assumptions (unconditional, strong, and weak) can be specified.
The behaviour of the system and the result of checking (violation or witness) can be shown as a computation tree and analyzed interactively.
