JISE

[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14]

Journal of Information Science and Engineering, Vol. 22 No. 2, pp. 357-373

Verification of UML Model Elements Using B

Ninh Thuan Truong and Jeanine Souquieres
LORIA - Universite Nancy
Nancy, France
E-mail: {truong; souquier}@loria.fr

We propose an approach to verify UML model elements based on the transformation of the UML meta-model into B formal specifications. The UML meta-model is described as a combination of graphical notations, natural and formal languages. The semantics of UML elements is expressed by well-formedness rules in the UML metamodel. Their correctness is ensured by the proof of the B specifications. The approach is illustrated by a simple case study: the printing system.

Keywords: B formal method, UML model and meta-model, formal verification, proof, transformation, well-formedness rules

Retrieve PDF document (JISE_200602_08.pdf)