Introduction

Pi2Promela is a compiler from pi-calculus models to Promela models. It serves as a front-end for Spin to model-check pi-calculus models against logical specifications described as LTL formulae.

Pi2Promela consists of two modules: one is a core module, namely a compilation engine, which is implemented in C; the other is a GUI module to provide a user-friendly interface(snapshot) , which is implemented in Java.

Download/Run

Pi2Promela is free to download and can run under the Windows 2000 or later, Unix/Linux operating systems.

The GUI module is built as a Java archive pi2promela.jar.
The core module is built as a Dynamic Link Library pi2pro.dll, and can also be extracted from the above Java archive. It is suggested that the DLL file be located in the same directory as the Java archive is, otherwise, the DLL file must be located within java.library.path.

To run the tool, "java -jar pi2promela.jar "

Case Study

Examples distributed with Mobility Workbench have been used for case studies. Download the source pi-calculus models with the corresponding Promela models.

Documentation

Peng Wu. Interpreting pi-Calculus with Spin/Promela. Computer Science, 2003, 8: 7 - 9, Supplement(the Proceedings of National Conference on Theoretical Computer Science, Qingdao, China, August 3 - 7, 2003. [An English version]

Citation

Thomas Noll and Chanchal Kumar Roy. Modeling Erlang in the pi-Calculus. In the Proceedings of 2005 ACM SIGPLAN Workshop on Erlang (ERLANG '05), pp. 72 - 77,Tallinn, Estonia, September 26 - 28, 2005. [abstract + full-text/ACM]