PIC2LNT Translator from Applied Pi-Calculus to LNT

Organisation:	CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
Functionality:	Translation from PIC (an applied pi-calculus) to LNT.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2010-2013
Description:	The pi-calculus was proposed by Milner, Parrow, and Walker about twenty years ago for describing concurrent systems with mobile communication. The pi-calculus is equipped with operational semantics defined in terms of LTSs (Labelled Transition Systems). Although a lot of theoretical results have been achieved on this language, only a few verification tools have been designed for analysing pi-calculus specifications automatically. The two most famous examples are the Mobility Workbench (MWB) and JACK, which were developed in the 90s. In this work, we extended the original polyadic pi-calculus with data-handling features. This results in a general-purpose applied pi-calculus, named PIC, which offers a good level of expressiveness for specifying mobile concurrent systems, and therefore for widening its possible application domains. For describing data types and functions in PIC, we adopted the LNT language, which provides constructive data type definitions and pattern-matching, in an imperative-like style with a user-friendly syntax. We first devised a translation from the finite control fragment of pi-calculus into LNT, taking care to map each transition of the pi-calculus term into one transition of the target LNT process. One key ingredient of the translation was the encoding of mobile communication channels using LNT data types. Then, we generalized it to handle PIC specifications, and we automated it in the tool PIC2LNT.
Conclusions:	Developing a compiler for a process calculus with mobility and data value communication is a complex task. We obtained such a compiler for an applied pi-calculus (PIC) with a reasonable effort by reusing the compiling and verification technology developed for classical process algebras (LNT). Our PIC2LNT translator enables the analysis of PIC specifications using all verification tools of CADP, in particular the EVALUATOR on-the-fly model checker, which can verify naturally temporal properties involving channel names and data values.
Publications:	[Mateescu-Salaun-10] Radu Mateescu and Gwen Salaün. Translating Pi-Calculus into LOTOS NT. Proceedings of the 8th International Conference on Integrated Formal Methods IFM'2010 (Nancy, France), LNCS vol. 6396, pp. 229-244. Springer Verlag, 2010. Available on-line at: http://hal.inria.fr/inria-00524586/en or from the CADP Web site in PDF or PostScript [Mateescu-Salaun-13] Radu Mateescu and Gwen Salaün. PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2013 (Rome, Italy), LNCS vol. 7795, pp.192-198. Springer Verlag, 2013. Available on-line at: http://hal.inria.fr/hal-00805533/en or from the CADP Web site in PDF or PostScript
Contact:	Radu Mateescu Inria Grenoble Rhône Alpes / CONVECS project-team 655, avenue de l'Europe 38330 Montbonnot FRANCE E-mail: Radu.Mateescu@inria.fr http://convecs.inria.fr/software/pic2lnt/
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page