Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, April 26, 2017 - 3:21:54 PM
Last modification on : Tuesday, October 19, 2021 - 4:09:38 PM
Long-term archiving on: : Thursday, July 27, 2017 - 12:54:36 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Dimitris Vekris, Catalin Dima. Efficient Operational Semantics for $ EB ^3$ for Verification of Temporal Properties. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.133-149, ⟨10.1007/978-3-642-40213-5_9⟩. ⟨hal-01514655⟩



Record views


Files downloads