Verification of EB3 Specifications Using CADP

Dimitris Vekris 1 Frédéric Lang 2, * Catalin Dima 1 Radu Mateescu 2
* Auteur correspondant
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : EB3 is a specification language for information systems. The core of the EB3 language consists of process algebraic specifications describing the behaviour of the entity types in a system, and attribute function definitions describing the entity attribute types. The verification of EB3 specifications against temporal properties is of great interest to users of EB3. In this paper, we propose a translation of EB3 to LOTOS NT (LNT for short), a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to EB3 and the LNT specification. We automated this translation with the EB32LNT tool, which makes it possible to verify EB3 specifications with the use of the CADP toolbox.
Type de document :
Communication dans un congrès
iFM 2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. 2013, 〈10.1007/978-3-642-38613-8_5〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00768310
Contributeur : Frederic Lang <>
Soumis le : vendredi 26 avril 2013 - 11:30:33
Dernière modification le : mercredi 11 avril 2018 - 01:56:24
Document(s) archivé(s) le : lundi 3 avril 2017 - 23:57:05

Fichier

paper3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Dimitris Vekris, Frédéric Lang, Catalin Dima, Radu Mateescu. Verification of EB3 Specifications Using CADP. iFM 2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. 2013, 〈10.1007/978-3-642-38613-8_5〉. 〈hal-00768310v4〉

Partager

Métriques

Consultations de la notice

606

Téléchargements de fichiers

107