The Psi-Calculi Workbench
Psi-Calculi Workbench (Pwb) is a parametric tool for concurrent system modeling and verification based on the Psi-calculi framework. It provides the usual concurrency primitives for modeling like the point-to-point message passing, broadcast message passing, non-determinism, and so on. The user just need to provide the data and logic for the messages and conditionals. The tool provides symbolic execution and behavioral equivalence generation (strong and weak bisimulation).
The tool comes with many examples on how use and implement the parameters.
Pwb is built with applications in mind, for example, sensor networks, security protocols, cache coherence protocols, etc. That is models that use different modes of communication, require structured data, and logics.
The tool is part of the UPMARC project tool set.
Pwb is open source software and the latest version is licensed under the BSD3.
You can obtain the latest source code from this git repository.
If you have bug reports, suggestions please open an issue on Github, or send a pull request.
Previous Source Code Releases
- 2011.09 - PsiWorkBench.tar.gz.
- Johannes Borgström, Ramunas Gutkovas, Ioana Rodhe, Björn Victor. The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi. ACM Trans. Embedded Comput. Syst. 14(1): 9:1-9:25 (2015). DOI
- Johannes Borgström, Ramunas Gutkovas, Ioana Rodhe, Björn Victor. A Parametric Tool for Applied Process Calculi. ACSD 2013: 180-185 PDF DOI