Translating FSP into LOTOS and Networks of Automata

Gwen Salaun 1 Jeff Kramer 2 Frederic Lang 1, * Jeff Magee 2
* Auteur correspondant
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. FSP is a widely-used calculus equipped with LTSA, a graphical and user-friendly tool. LOTOS is the only process calculus that has led to an international standard, and is supported by the CADP verification toolbox. We propose a translation from FSP to LOTOS. Since FSP composite processes are hard to encode into LOTOS, they are translated into networks of automata which are another input language accepted by CADP. Hence, it is possible to use jointly LTSA and CADP to validate FSP specifications. Our approach is completely automated by a translator tool we implemented.
Type de document :
Communication dans un congrès
6th International Conference on Integrated Formal Methods IFM'2007, Jul 2007, Oxford, United Kingdom. 2007
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00198731
Contributeur : Frederic Lang <>
Soumis le : lundi 17 décembre 2007 - 18:21:51
Dernière modification le : jeudi 11 janvier 2018 - 06:22:03
Document(s) archivé(s) le : lundi 12 avril 2010 - 08:14:00

Fichier

Salaun-Kramer-Lang-Magee-07.pd...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00198731, version 1

Collections

Citation

Gwen Salaun, Jeff Kramer, Frederic Lang, Jeff Magee. Translating FSP into LOTOS and Networks of Automata. 6th International Conference on Integrated Formal Methods IFM'2007, Jul 2007, Oxford, United Kingdom. 2007. 〈inria-00198731〉

Partager

Métriques

Consultations de la notice

277

Téléchargements de fichiers

110