Organisation: 
CONVECS projectteam, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)


Functionality: 
Translation from PIC (an applied picalculus) to LNT.

Tools used: 
CADP (Construction and Analysis of Distributed Processes)

Period: 
20102013

Description: 
The picalculus was proposed by Milner, Parrow, and Walker about twenty
years ago for describing concurrent systems with mobile communication.
The picalculus 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 picalculus 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 picalculus with datahandling features. This results in a generalpurpose applied picalculus, 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 patternmatching, in an imperativelike style with a userfriendly syntax. We first devised a translation from the finite control fragment of picalculus into LNT, taking care to map each transition of the picalculus 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 picalculus (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 onthefly model checker, which can verify naturally temporal
properties involving channel names and data values.

Publications: 
[MateescuSalaun10]
Radu Mateescu and Gwen Salaün.
Translating PiCalculus into LOTOS NT.
Proceedings of the 8th International Conference on Integrated Formal
Methods IFM'2010 (Nancy, France), LNCS vol. 6396, pp. 229244.
Springer Verlag, 2010.
Available online at: http://hal.inria.fr/inria00524586/en or from the CADP Web site in PDF or PostScript [MateescuSalaun13] Radu Mateescu and Gwen Salaün. PIC2LNT: Model Transformation for Model Checking an Applied PiCalculus. 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.192198. Springer Verlag, 2013. Available online at: http://hal.inria.fr/hal00805533/en or from the CADP Web site in PDF or PostScript 
Contact:  Radu Mateescu Inria Grenoble Rhône Alpes / CONVECS projectteam 655, avenue de l'Europe 38330 Montbonnot FRANCE Email: 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 