An OCL extension for checking and transforming UML models

The increasing use of models in specification and design phases makes them first class citizens. Models which had, till now, been used to gain a better grasp of the software to be designed, have been attributed a productive role that has become central to development. This new status of models and meta-models poses the problem of how they are established and especially, how they are validated. So, each activity in a process can be supported by MDE (Model-Driven Engineering) components realizing transformations and verifications. These operations require redefining the OCL type system for taking into account multi-model handling and side-effects. Checking the transformation consists of ensuring that the source models and the targets respect a set of properties that can be verified through transformation contracts. The NEPTUNE platform was designed having this logic as a driving force - allowing the verification of models and of their transformation.