On the Specification, Verification and Implementation of Model Transformations with Transformation Contracts

  • Christiano Braga
  • Roberto Menezes
  • Thiago Comicio
  • Cassio Santos
  • Edson Landim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)


Model transformations are first-class artifacts in a model-driven development process. As such, their verification and validation is an important task. We have been developing a technique to specify, verify, validate and implement model transformations. Our technique is based on the concept of transformation contracts, a specification that relates two modeling languages and declares properties that must be fulfilled in such a relation. A transformation contract is essentially a transformation model that allows for the verification and validation of a model transformation using the same techniques one uses to verify and validate any given model. This paper describes our technique, discusses consistency of model transformations and reports on its application to a model transformation from access control models to Java security.


Modeling Language Model Transformation Design Pattern Description Logic Class Diagram 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Akehurst, D.H., Kent, S.: A relational approach to defining transformations in a metamodel. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 243–258. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Baader, F., Diego Calvanese, D.M., Nardi, D., Patel-Schneider, P.: The Description Logic Handbook. Cambridge University Press (2003)Google Scholar
  3. 3.
    Basin, D., Clavel, M., Doser, J., Egea, M.: Automated analysis of security-design models. Inf. Softw. Technol. 51(5), 815–831 (2009)CrossRefGoogle Scholar
  4. 4.
    Basin, D., Doser, J., Lodderstedt, T.: Model driven security: From uml models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15(1), 39–91 (2006)CrossRefGoogle Scholar
  5. 5.
    Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams. Artif. Intellig. 168, 70–118 (2005)CrossRefzbMATHGoogle Scholar
  6. 6.
    Bézivin, J., Büttner, F., Gogolla, M., Jouault, F., Kurtev, I., Lindow, A.: Model Transformations? Transformation Models! In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199, pp. 440–453. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Braga, C.: From access control policies to an aspect-based infrastructure: A metamodel-based approach. In: Chaudron, M.R.V. (ed.) MODELS 2008. LNCS, vol. 5421, pp. 243–256. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Braga, C.: A transformation contract to generate aspects from access control policies. J. of Software and Systems Modeling (2010), doi:10.1007/s10270-010-0156-xGoogle Scholar
  9. 9.
    Braga, C., Hæusler, E.H.: Lightweight analysis of access control models with description logic. Innov. in Systems and Soft. Eng. 6, 115–123 (2010)CrossRefGoogle Scholar
  10. 10.
    Cariou, E., Marvie, R., Seinturier, L., Duchien, L.: OCL for the specification of model transformation contracts. In: Proc. of OCL and Model Driven Eng. Work., pp. 69–83 (2004)Google Scholar
  11. 11.
    Clavel, M., Egea, M., de Dios Miguel Angel, G.: Building an efficient component for OCL evaluation. ECEASST 15 (2008)Google Scholar
  12. 12.
    Comicio, T.: A transformation contract approach for model-driven security. Master’s thesis, Universidade Federal Fluminense (2011)Google Scholar
  13. 13.
    Egea, M.: An Executable Formal Semantics for OCL with Applications to Model Analysis and Validation. PhD thesis, Universidad Complutense de Madrid (2008)Google Scholar
  14. 14.
    Gorp, P.V., Janssens, D.: Cavit: a consistency maintenance framework based on transformation contracts. In: Transformation Techniques in Soft. Eng., Dagstuhl Seminar Proc., vol. 05161 (2006)Google Scholar
  15. 15.
    Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained. Addison-Wesley, Reading (2003)Google Scholar
  16. 16.
    OMG. MOF QVT final adopted specification, omg adopted specification ptc/05-11-01 (2005)Google Scholar
  17. 17.
    Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Christiano Braga
    • 1
  • Roberto Menezes
    • 1
  • Thiago Comicio
    • 1
  • Cassio Santos
    • 1
  • Edson Landim
    • 1
  1. 1.Instituto de ComputaçãoUniversidade Federal FluminenseBrazil

Personalised recommendations