K. Anastasakis, B. Bordbar, G. Georg, and I. Ray, On challenges of model transformation from UML to Alloy. Software and Systems Modeling, pp.69-86, 2010.

K. Anastasakis, B. Bordbar, and J. Küster, Analysis of model transformations via alloy, MODEVVA'07, 2007.

R. Back and J. Wright, Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science, 1998.
DOI : 10.1007/978-1-4612-1674-2

J. Bézivin, F. Büttner, M. Gogolla, F. Jouault, I. Kurtev et al., Model transformations? Transformation models! In MoDELS'06, LNCS, vol.4199, 2006.

F. Büttner, M. Egea, and J. Cabot, On verifying ATL transformations using offthe-shelf SMT solvers, MoDELS'12, pp.432-448, 2012.

F. Büttner, M. Egea, J. Cabot, and M. Gogolla, Verification of ATL Transformations Using Transformation Models and Model Finders, ICFEM'12, pp.198-213, 2012.
DOI : 10.1007/978-3-642-34281-3_16

J. Cabot, R. Clarisó, E. Guerra, and J. De-lara, Verification and validation of declarative model-to-model transformations through invariants, Journal of Systems and Software, vol.83, issue.2, pp.283-302, 2010.
DOI : 10.1016/j.jss.2009.08.012

URL : https://hal.archives-ouvertes.fr/hal-00540816

J. Cabot, R. Clarisó, and D. Riera, UMLtoCSP, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering , ASE '07, 2007.
DOI : 10.1145/1321631.1321737

E. Cariou, R. Marvie, L. Seinturier, and L. Duchien, OCL for the specification of model transformation contracts, OCL Workshop, pp.69-83, 2004.

M. Clavel, M. Egea, and M. A. De-dios, Checking Unsatisfiability for OCL Constraints, Electronic Communications of the EASST, vol.24, pp.1-13, 2009.

E. Guerra, Specification-Driven Test Generation for Model Transformations, ICMT'12, pp.40-55, 2012.
DOI : 10.1007/978-3-642-30476-7_3

URL : http://hdl.handle.net/10486/664296

E. Guerra, J. De-lara, D. Kolovos, R. Paige, and O. Santos, Engineering model transformations with transML. Software and Systems Modeling, 2012.

E. Guerra, J. De-lara, D. S. Kolovos, and R. F. Paige, A Visual Specification Language for Model-to-Model Transformations, 2010 IEEE Symposium on Visual Languages and Human-Centric Computing, pp.119-126, 2010.
DOI : 10.1109/VLHCC.2010.25

E. Guerra, J. De-lara, M. Wimmer, G. Kappel, A. Kusel et al., Automated verification of model transformations based on visual contracts, Automated Software Engineering, vol.32, issue.8, pp.5-46, 2013.
DOI : 10.1007/s10515-012-0102-y

D. Jackson, Software Abstractions -Logic, Language, and Analysis, 2012.

F. Jouault, F. Allilaire, J. Bézivin, and I. Kurtev, ATL: A model transformation tool, Science of Computer Programming, vol.72, issue.1-2, pp.31-39, 2008.
DOI : 10.1016/j.scico.2007.08.002

URL : https://hal.archives-ouvertes.fr/hal-00483363

M. Kuhlmann, L. Hamann, and M. Gogolla, Extensive Validation of OCL Models by Integrating SAT Solving into USE, LNCS, vol.6705, issue.11, pp.290-306, 2011.
DOI : 10.1007/978-3-642-21952-8_21

F. Orejas and M. Wirsing, On the Specification and Verification of Model Transformations, LNCS, vol.152, issue.1, pp.140-161, 2009.
DOI : 10.1007/3-540-59071-4_45

A. Queralt and E. Teniente, Verification and Validation of UML Conceptual Schemas with OCL Constraints, ACM Transactions on Software Engineering and Methodology, vol.21, issue.2, p.13, 2012.
DOI : 10.1145/2089116.2089123

A. Schürr, Specification of graph translators with triple graph grammars, WG'94, pp.151-163, 1994.
DOI : 10.1007/3-540-59071-4_45

J. M. Spivey, An introduction to Z and formal specifications, Software Engineering Journal, vol.4, issue.1, pp.40-50, 1989.
DOI : 10.1049/sej.1989.0006

A. Vallecillo and M. Gogolla, Typing Model Transformations Using Tracts, ICMT'12, pp.56-71, 2012.
DOI : 10.1007/978-3-642-30476-7_4