$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.