Efficient Operational Semantics for $ EB ^3$ for Verification of Temporal Properties

Abstract : $ EB ^3$ is a specification language for information systems. The core of the $ EB ^3$ 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 $ EB ^3$ specifications against temporal properties is of great interest to users of $ EB ^3$. We give here an operational semantics for $ EB ^3$ programs in which attribute functions are computed during program evolution and their values are stored into program memory. By assuming that all entities have finite domains, this gives a finitary operational semantics. We then demonstrate how this new semantics facilitates the translation of $ EB ^3$ specifications to LOTOS NT (LNT for short) for verification of temporal properties with the use of the CADP toolbox.
Type de document :
Communication dans un congrès
Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.133-149, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_9〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01514655
Contributeur : Hal Ifip <>
Soumis le : mercredi 26 avril 2017 - 15:21:54
Dernière modification le : jeudi 27 avril 2017 - 01:06:20
Document(s) archivé(s) le : jeudi 27 juillet 2017 - 12:54:36

Fichier

978-3-642-40213-5_9_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Dimitris Vekris, Catalin Dima. Efficient Operational Semantics for $ EB ^3$ for Verification of Temporal Properties. Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.133-149, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_9〉. 〈hal-01514655〉

Partager

Métriques

Consultations de la notice

130

Téléchargements de fichiers

23