Efficient Operational Semantics for EB3 for Verification of Temporal Properties

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. We give here an operational semantics for EB3 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 EB3 specifications to LOTOS NT (LNT for short) for verification of temporal properties with the use of the CADP toolbox.