Verification of EB3 specifications using CADP

Abstract : EB3 is a specification language for information systems. The core of the EB language consists of process algebraic specifications describing the behaviour of the entities in a system, and attribute function definitions describing the entity attributes. The verification of eb3 specifications against temporal properties is of great interest to users of EB3. In this paper, we propose a translation from 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 the EB3 and LNT specifications. We automated this translation with the EB32LNT tool, thus equipping the EB3 method with the functional verification features available in the CADP toolbox.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2016, 28 (1), pp.145-178. 〈10.1007/s00165-016-0362-6〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01290460
Contributeur : Frederic Lang <>
Soumis le : mardi 29 mars 2016 - 10:47:52
Dernière modification le : jeudi 11 janvier 2018 - 06:23:43
Document(s) archivé(s) le : lundi 14 novembre 2016 - 07:05:20

Fichier

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

Identifiants

Collections

Citation

Dimitris Vekris, Frédéric Lang, Catalin Dima, Radu Mateescu. Verification of EB3 specifications using CADP . Formal Aspects of Computing, Springer Verlag, 2016, 28 (1), pp.145-178. 〈10.1007/s00165-016-0362-6〉. 〈hal-01290460〉

Partager

Métriques

Consultations de la notice

225

Téléchargements de fichiers

65