Introduction
The π-calculus [12] was proposed by Milner, Parrow, and Walker about twenty years ago for describing concurrent systems with mobile communication. The π-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 (see, e.g., [1, chapter 8] for a survey), only a few verification tools have been designed for analysing π-calculus specifications automatically. The two most famous examples are the Mobility Workbench (Mwb) [14] and Jack [5], which were developed in the 90s.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier (2001)
Blanchet, B., Smyth, B.: Proverif: Automatic cryptographic protocol verifier, user manual and tutorial, version 1.86pl3 (2011)
Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference manual of the LOTOS NT to LOTOS translator (version 5.1). Inria/Vasy, 109 pages (2010)
Dam, M.: Model Checking Mobile Processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 22–36. Springer, Heidelberg (1993)
Ferrari, G., Ferro, G., Gnesi, S., Montanari, U., Pistore, M., Ristori, G.: An Automata Based Verification Environment for Mobile Processes. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 275–289. Springer, Heidelberg (1997)
Garavel, H.: OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)
Garavel, H., Lang, F., Mateescu, R.: Compiler Construction Using LOTOS NT. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol. 2304, pp. 9–13. Springer, Heidelberg (2002)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Mateescu, R., Salaün, G.: Translating Pi-Calculus into LOTOS NT. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 229–244. Springer, Heidelberg (2010)
Mateescu, R., Salaün, G.: Pic2Lnt: A translator from the applied pi-calculus to LOTOS NT (2012), http://convecs.inria.fr/software
Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inf. Comput. 100(1), 1–77 (1992)
Montanari, U., Pistore, M.: Checking Bisimilarity for Finitary π-Calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 42–56. Springer, Heidelberg (1995)
Victor, B., Moller, F.: The Mobility Workbench – A Tool for the π-Calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mateescu, R., Salaün, G. (2013). PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. In: Piterman, N., Smolka, S.A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013. Lecture Notes in Computer Science, vol 7795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36742-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-36742-7_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36741-0
Online ISBN: 978-3-642-36742-7
eBook Packages: Computer ScienceComputer Science (R0)