A Formal Approach for the Specification and the Verification of UML Structural Properties: Application to E-Business Domain

This paper presents a formal approach for the specification and the verification of UML diagrams against a set of structural properties. This work is part of the E-fficient research project, aiming at building correct e-business processes. An e-business process is described using class and activity diagrams. The verification of structural properties gives a degree of confidence regarding the correctness of the related business process. Our proposal is based on the formal approach promoted by the USE tool. The USE approach aims at validating a particular state of an object model against properties described in OCL. The contributions of this paper are: the introduction of meta-model based on class diagrams for UML diagrams to be verified, rules for the translation of the class, object and activity diagrams into USE specifications, and the specification of structural properties in OCL.