A. Consortium, AUTOSAR System Template, 2007.

K. Anastasakis, B. Bordbar, and J. Küster, Analysis of Model Transformations via Alloy. MoDeVVa, pp.47-56, 2007.

M. Asztalos, L. Lengyel, and T. Levendovszky, Towards Automated, Formal Verification of Model Transformations, 2010 Third International Conference on Software Testing, Verification and Validation, pp.15-24, 2010.
DOI : 10.1109/ICST.2010.42

L. Baresi and P. Spoletini, On the Use of Alloy to Analyze Graph Transformation Systems, ICGT, pp.306-320, 2006.
DOI : 10.1007/11841883_22

B. Becker, L. Lambers, J. Dyck, S. Birth, and H. Giese, Iterative Development of Consistency-Preserving Rule-Based Refactorings, pp.123-137, 2011.
DOI : 10.1007/978-3-642-21732-6_9

C. Braga, R. Menezes, T. Comicio, C. Santos, and E. Landim, On the Specification, Verification and Implementation of Model Transformations with Transformation Contracts, SBMF, pp.108-123, 2011.
DOI : 10.1007/3-540-59071-4_45

A. D. Brucker and B. Wolff, Semantics, calculi, and analysis for object-oriented specifications, Acta Informatica, vol.39, issue.2, pp.255-284, 2009.
DOI : 10.1007/s00236-009-0093-8
URL : https://hal.archives-ouvertes.fr/hal-01214519

F. Büttner, M. Egea, and J. Cabot, On Verifying ATL Transformations Using ???off-the-shelf??? SMT Solvers, MODELS, pp.432-448, 2012.
DOI : 10.1007/978-3-642-33666-9_28

F. Büttner, M. Egea, J. Cabot, and M. Gogolla, Verification of ATL Transformations Using Transformation Models and Model Finders, In ICFEM LNCS, vol.7635, 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

E. Cariou, N. Belloir, F. Barbier, and N. Djemam, OCL Contracts for the Verification of Model Transformations, p.24, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01093481

T. Cottenier, A. Van-den, T. Berg, and . Elrad, The Motorola WEAVR: Model Weaving in a Large Industrial Context, AOSD, 2007.

A. Daghsen, K. Chaaban, S. Saudrais, and P. Leserf, Applying Holistic Distributed Scheduling to AUTOSAR Methodology, ERTSS, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00660252

H. Giese, S. Hildebrandt, and S. Neumann, Model Synchronization at Work: Keeping SysML and AUTOSAR Models Consistent. Graph Transformations and Model-Driven Engineering, pp.555-579, 2010.

M. Gogolla and A. Vallecillo, Tractable Model Transformation Testing, ECMFA, pp.221-236, 2011.
DOI : 10.1007/978-3-642-21470-7_16

C. A. González-pérez, F. Büttner, R. Clarisó, and J. Cabot, EMFtoCSP: A tool for the lightweight verification of EMF models, 2012 First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA), pp.44-50, 2012.
DOI : 10.1109/FormSERA.2012.6229788

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

K. Inaba, S. Hidaka, Z. Hu, H. Kato, and K. Nakano, Graph-transformation verification using monadic second-order logic, Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming, PPDP '11, pp.17-28, 2011.
DOI : 10.1145/2003476.2003482

E. Jackson, T. Levendovszky, and D. Balasubramanian, Automatically reasoning about metamodeling. SoSyM, pp.1-15, 2013.

B. Jacobs and E. Poll, A Logic for the Java Modeling Language JML, FASE, pp.284-299, 2001.
DOI : 10.1007/3-540-45314-8_21

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, TOOLS, pp.290-306, 2011.
DOI : 10.1007/978-3-642-21952-8_21

L. Lúcio, B. Barroca, and V. Amaral, A Technique for Automatic Validation of Model Transformations, MODELS, pp.136-150, 2010.
DOI : 10.1007/978-3-642-16145-2_10

P. Mohagheghi and V. Dehlen, Where Is the Proof? - A Review of Experiences from Applying MDE in Industry, ECMDA?FA, pp.432-443, 2008.
DOI : 10.1007/978-3-540-69100-6_31

A. Narayanan and G. Karsai, Verifying Model Transformations by Structural Correspondence, EASST, vol.10, issue.0, 2008.

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. Rensink, Explicit State Model Checking for Graph Grammars, Concurrency, Graphs and Models, pp.114-132, 2008.
DOI : 10.1007/978-3-540-68679-8_8

G. Selim, S. Wang, J. Cordy, and J. Dingel, Model Transformations for Migrating Legacy Models: An Industrial Case Study, ECMFA, pp.90-101, 2012.
DOI : 10.1007/978-3-642-31491-9_9

S. Sen, N. Moha, B. Baudry, and J. Jézéquel, Meta-model Pruning, MOD- ELS, pp.32-46, 2009.
DOI : 10.1016/S1571-0661(04)80066-5
URL : https://hal.archives-ouvertes.fr/inria-00468514

K. Stenzel, N. Moebius, and W. Reif, Formal Verification of QVT Transformations for Code Generation, MODELS, pp.533-547, 2011.

M. Tisi, F. Jouault, P. Fraternali, S. Ceri, and J. Bézivin, On the Use of Higher-Order Model Transformations, ECMDA-FA, 2009.
DOI : 10.1007/978-3-540-69927-9_11
URL : https://hal.archives-ouvertes.fr/hal-00782464

E. Torlak and D. Jackson, Kodkod: A Relational Model Finder, TACAS, 2007.
DOI : 10.1007/978-3-540-71209-1_49

J. Troya and A. Vallecillo, A Rewriting Logic Semantics for ATL., The Journal of Object Technology, vol.10, issue.5, pp.1-29, 2011.
DOI : 10.5381/jot.2011.10.1.a5