SyncStitch is a tool for designing concurrent systems based on the process algebra CSP (Communicating Sequential Processes). Using SyncStitch, you can model, simulate, and check concurrent systems such as multi-threading applications, embedded systems, and network programs.
SyncStitch provides two ways for modeling the behavior of systems:
Process expressions are text descriptions of the behavior of systems, which are written in a special language based on the programming language Scheme.
The language has elements for describing event synchronizations and channel communications, and you can describe interactions between systems in addition to the behavior of the systems.
You can run the system on SyncStitch as soon as you model it. This execution is generally called simulation. In contrast to the usual execution of programs, model simulation shows the behavior of the system as a computation tree. You can look over and investigate the behavior of the system on the tree. You can see the transitions in each state, inspect the structure of the process, and examine the values of variables in the state.
SyncStitch provides four methods to check models:
You can check whether the implementation model you designed satisfies the behavioral specification with these methods. The behavioral specification is needed to be described as a model. You can also check whether the behavioral specification satisfies the requirements related to the behavior of the system if you model the conditions of the requirements as models.
For more information about SyncStitch, please read SyncStitch User Guide in the trial version of SyncStitch.