An OCL-based technique for specifying and verifying refinement-oriented transformations in MDE

Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea (Cons. 11/03/2009)

Despite the fact that the refinement technique is one of the cornerstones of a formal approach to software engineering, the concept of refinement in model driven engineering is loosely defined and open to misinterpretations. In this article we present a rigorous technique for specifying and verifying frequently occurring forms of refinement that take place in software modeling. Such strategy uses the formal language Object-Z as a background foundation, whereas designers only have to deal with the broadly accepted UML and OCL languages, thus propitiating the inclusion of verification in ordinary software engineering activities, increasing in this way the level of confidence on the correctness of the final product. Finally, an automatic tool is provided to support such model refinement activities; this tool adopts the micromodels strategy to reduce the search scope, making the verification process feasible.

David Harel, Gianna Reggio, Oscar Nierstrasz, Jon Whittle. Proceedings MoDELS/UML 2006 Model Driven Engineering Languages and Systems, 9th International Conference, 2006, Lecture Notes in Computer Science.