Previous 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 (March 2006)

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

Full Text (¥þ¤åÀÉ) Retrieve PDF document (200603_08.pdf)

Received July 1, 2005; accepted November 24, 2005.
Communicated by Sung Shin.