ProPi is a tool that statically verifies whether message passing programs are free from deadlocks.
Propi takes as input a system specified in the pi-calculus, together with typing annotations that describe the communications in the channels, as well as event annotations so as to capture the overall ordering of the communications. The tool produces as result either a positive answer (the system type checks), in which case the properties of protocol fidelity (system communications follow the typing prescription) and progress (deadlock absence) hold. Otherwise, the system exhibits error information so as to allow to identify what is the problem in the system specification. The tool includes an Eclipse plugin and a standalone command line interface.
Team
Downloads
Running from Eclipse
Requirements
- An Eclipse IDE installed
Installing and using the Eclipse ProPi Plugin
- In Eclipse go to the Help menu → Install New Software
- In the Work with field introduce : http://download.gloss.di.fc.ul.pt/propi/update/
- Select the SDK Feature and press Next
- Restart Eclipse
- Create a Project or Java Project
- Create a file with extension “.p” and select yes when the editor asks to add the Xtext nature to your project
- Write a program on the created file (see examples below) and press save to verify
Running from the command line
- Download ProPi.jar
- Create a new file with extension .p
- Using the command type: java -jar ProPi.jar
- Specify the specific or relative path to the communicating program file or to a folder contaning multiple program files
Examples
- Professor, student, and an assistant
- Buyers and seller communicating program
- Deadlocked communicating program
- A shared service with an handle delegation
- A shared service with a shared masterservice delegation
- Bigger type sequence with multiple shared channels delegations
- Confluent synchronizations
Publications
-
-
- André Camacho, Tools and Techniques for the Static Verification of Progress in Communication-Centred Systems, Master’s thesis, University of Lisbon, 2014 (thesis)
- Hugo T. Vieira and Vasco T. Vasconcelos, Typing Progress in Communication-Centred Systems, Coordination’13 Proceedings, LNCS Vol 7890:236-250, Springer, 2013 (SpringerLink, Preprint)
- Vasco T. Vasconcelos, Fundamentals of Session Types, Information and Computation, Elsevier, 217:52-70, 2012 (ScienceDirect)
-