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.