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 language based on CSP and a typed functional programming language.
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 states.
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.
SyncStich can boost your design skills and improve the quality of your products. Please download SyncStitch and try it!