Verification of EB3 specifications using CADPReportar como inadecuado

Verification of EB3 specifications using CADP - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LACL - Laboratoire d-Algorithmique Complexité et Logique 2 CONVECS - Construction of verified concurrent systems Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d-Informatique de Grenoble

Abstract : EB3 is a specification language for information systems. The core of the EB language consists ofprocess algebraic specifications describing the behaviour of the entities in a system, and attribute functiondefinitions describing the entity attributes. The verification of eb3 specifications against temporal propertiesis of great interest to users of EB3. In this paper, we propose a translation from EB3 to LOTOS NT LNT forshort, a value-passing concurrent language with classical process algebra features. Our translation ensuresthe one-to-one correspondence between states and transitions of the labelled transition systems correspondingto the EB3 and LNT specifications. We automated this translation with the EB32LNT tool, thus equippingthe EB3 method with the functional verification features available in the CADP toolbox.

Autor: Dimitris Vekris - Frédéric Lang - Catalin Dima - Radu Mateescu -



Documentos relacionados