UML/OCL and Refinement

Formal methods such as B and Event-B support the achievement of correct systems design using the refinement technique. These methods allow for the description of data and actions at different levels of abstraction. The OCL provides some precision to UML models. The means offered by OCL Collection, Set, OrderedSet, Bag and Sequence are insufficient to support an incremental process of class diagrams development based on technical refinement. Indeed, the description of an initial model often requires very abstract mathematical concepts such as relation and function. These concepts are difficult to express in OCL using TupleType and def. This discourages the designer from expressing abstract constraints. Moreover, the absence of these concepts does not favor the move from semi-formal to formal: UML/OCL to Event-B. To overcome these flaws, we propose an OCL mathematical extension by increasing its class library.