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.