Skip to main content
Department of Information Technology

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.

Publications

  • 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
Updated  2016-12-22 19:51:38 by Ramunas Gutkovas.