Verification of EB3 specifications using CADP

Dimitris Vekris, Frédéric Lang, Catalin Dima, and Radu Mateescu

Formal Aspects of Computing, 28(1):145-178, 2016

Abstract:

EB3 is a specication language for information systems. The core of the EB3 language consists of process algebraic specications describing the behaviour of the entities in a system, and attribute function denitions describing the entity attributes. The verication of EB3 specications 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 specications. We automated this translation with the EB32LNT tool, thus equipping the EB3 method with the functional verication features available in the CADP toolbox.

34 pages

PDF

PostScript