PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus

Radu Mateescu 1, * Gwen Salaün 1
* Auteur correspondant
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : In this paper, we present an applied pi-calculus obtained by extending Milner's pi-calculus with data types and expressions. The applied pi-calculus is automatically translated to the LNT value-passing process specification language by means of the PIC2LNT 2.0 tool. This enables the verification of applied pi-calculus specifications by using the data-based temporal logics and the model checkers of the CADP toolbox.
Type de document :
Communication dans un congrès
Nir Piterman and Scott Smolka. TACAS - 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - 2013, Mar 2013, Rome, Italy. Springer, 7795, pp.192-198, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-36742-7_14〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00805533
Contributeur : Radu Mateescu <>
Soumis le : jeudi 28 mars 2013 - 10:35:20
Dernière modification le : mercredi 11 avril 2018 - 01:53:07
Document(s) archivé(s) le : samedi 29 juin 2013 - 04:02:57

Fichier

Mateescu-Salaun-13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | CONVECS | LIG_MFML_CONVECS | LIG_MFML | LIG | UGA | LIG_SRCPR | INRIA-RENGRE

Citation

Radu Mateescu, Gwen Salaün. PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. Nir Piterman and Scott Smolka. TACAS - 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - 2013, Mar 2013, Rome, Italy. Springer, 7795, pp.192-198, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-36742-7_14〉. 〈hal-00805533〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

487

Téléchargements de fichiers

142

Contact


archive-ouverte@inria.fr