[1] 
Esther Guerra, Juan de Lara, Dimitrios S. Kolovos, Richard F. Paige, and Osmar Marchi dos Santos. Engineering model transformations with transml. Software & Systems Modeling, 12(3):555577, Jul 2013. [ bib  DOI ]
Model transformation is one of the pillars of modeldriven engineering (MDE). The increasing complexity of systems and modelling languages has dramatically raised the complexity and size of model transformations as well. Even though many transformation languages and tools have been proposed in the last few years, most of them are directed to the implementation phase of transformation development. In this way, even though transformations should be built using sound engineering principlesjust like any other kind of softwarethere is currently a lack of cohesive support for the other phases of the transformation development, like requirements, analysis, design and testing. In this paper, we propose a unified family of languages to cover the life cycle of transformation development enabling the engineering of transformations. Moreover, following an MDE approach, we provide tools to partially automate the progressive refinement of models between the different phases and the generation of code for several transformation implementation languages.

[2] 
Dan Song, Keqing He, Peng Liang, and Wudong Liu. A Formal Language for Model Transformation Specification. In ICEIS (3), pages 429433, 2005. [ bib  DOI ] 
[3] 
SoonKyeong Kim, David Carrington, and Roger Duke. A metamodelbased transformation between UML and ObjectZ. In Proceedings IEEE Symposia on HumanCentric Computing Languages and Environments (Cat. No.01TH8587), pages 112119. Proceedings IEEE Symposia on HumanCentric Computing Languages and Environments (Cat. No.01TH8587), Sep. 2001. [ bib  DOI ]
Keywords: specification languages;objectoriented languages;visual languages;metamodelbased transformation;UML;ObjectZ;formal modeling notations;visual modeling notations;software models;imprecise incomplete inconsistent transformation task;metalevel transformation;case study;visual representation;specification;Unified modeling language;Formal specifications;Object oriented modeling;Computer science;Australia;Software systems;Performance analysis;Bidirectional control;Specification languages

[4] 
Nazir Ahmad Zafar and Fahad Alhumaidan. Transformation of class diagrams into formal specification. International Journal of Computer Science and Network Security, 11(5):289295, 2011. [ bib ] 
[5] 
Jim Woodcock and Jim Davies. Using Z: specification, refinement, and proof. PrenticeHall, Inc., 1996. [ bib ] 
[6] 
Frédéric Jouault, Freddy Allilaire, Jean Bézivin, and Ivan Kurtev. ATL: A model transformation tool. Science of Computer Programming, 72(1):3139, 2008. [ bib  DOI ] 
[7] 
Dan Li, Xiaoshan Li, and Volker Stolz. QVTbased Model Transformation Using XSLT. SIGSOFT Softw. Eng. Notes, 36(1):18, January 2011. [ bib  DOI ]
Keywords: QVT relations, XSLT, graphical notation, model transformations

[8] 
Jean Bézivin. On the unification power of models. Software & Systems Modeling, 4(2):171188, May 2005. [ bib  DOI ]
In November 2000, the OMG made public the MDAinitiative, a particular variant of a new global trend called MDE (Model Driven Engineering). The basic ideas of MDA are germane to many other approaches such as generative programming, domain specific languages, modelintegrated computing, generic model management, software factories, etc. MDA may be defined as the realization of MDE principles around a set of OMG standards like MOF, XMI, OCL, UML, CWM, SPEM, etc. MDE is presently making several promises about the potential benefits that could be reaped from a move from codecentric to modelbased practices. When we observe these claims, we may wonder when they may be satisfied: on the short, medium or long term or even never perhaps for some of them. This paper tries to propose a vision of the development of MDE based on some lessons learnt in the past 30 years in the development of object technology. The main message is that a basic principle (“Everything is an object”) was most helpful in driving the technology in the direction of simplicity, generality and power of integration. Similarly in MDE, the basic principle that “Everything is a model” has many interesting properties, among others the capacity to generate a realistic research agenda. We postulate here that two core relations (representation and conformance) are associated to this principle, as inheritance and instantiation were associated to the object unification principle in the classbased languages of the 80's. We suggest that this may be most useful in understanding many questions about MDE in general and the MDA approach in particular. We provide some illustrative examples. The personal position taken in this paper would be useful if it could generate a critical debate on the research directions in MDE.

[9] 
Jean Bézivin and Frédéric Jouault. Using ATL for checking models. Electronic Notes in Theoretical Computer Science, 152:6981, 2006. [ bib  DOI ] 
[10] 
Nuno Amálio and Fiona Polack. Comparison of formalisation approaches of uml class constructs in Z and ObjectZ. In Didier Bert, Jonathan P. Bowen, Steve King, and Marina Waldén, editors, ZB 2003: Formal Specification and Development in Z and B, pages 339358, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. [ bib  DOI ]
UML, and other objectoriented approaches to system specification and design, are increasingly popular in industry. Many attempts have been made to formalise either the notations, the system models produced using these notations, or both. However, there have been no attempts to compare the expressiveness of the formal approaches. This paper compares Z and ObjectZ approaches to objectoriented formalisation. The Z approaches reflect different formalisation goals (a formal model of the system, a formal model of a diagrammatic objectoriented model). The ObjectZ approach produces compact formal models, but imposes a particular semantic interpretation on the UML notations.

[11] 
Anneke G Kleppe, Jos B Warmer, and Wim Bast. MDA explained, the model driven architecture: Practice and promise. AddisonWesley Professional, 2003. [ bib ] 
[12] 
C. Amelunxen. Formalising model transformation rules for UML/MOF 2. IET Software, 2:204222(18), June 2008. [ bib  DOI ]
Modeldriven software development, today's stateoftheart approach to the design of software, can be applied in various domains and thus demands a variety of domainspecific modelling languages. The specification of a domainspecific modelling language's syntax and semantics can in turn be specified based on models, which represent the approach of metamodelling as a special form of language engineering. The latest version of the unified modelling language 2 (UML 2) and its subset the meta object facility 2 (MOF 2) provide sufficient support for metamodelling, a modelling language's abstract syntax. Furthermore, based on the description of the abstract syntax, a language's static semantics can simply be specified by the object constraint language (OCL) as UML/MOF's natural constraint language, whereas the description of an MOF compliant language's dynamic semantics is still not covered. The authors try to close this gap by integrating MOF/OCL with graph transformations for the specification of dynamic aspects of modelling languages and tools. The formalisation of such an integration is nontrivial because of the fact that UML/MOF 2 offer a rather unusual and sophisticated association concept (graph model). Although there are many approaches, which formalise graph transformations in general and first approaches that offer a precise specification of the semantics of the association concepts of UML/MOF 2, there is still a lack in bringing both together. Here, the authors close this gap by formalising graph transformations that work on a UML/MOF 2 compatible graph model.
Keywords: domainspecific modelling language syntax;meta object facility 2;object constraint language;modeldriven software development;UML;Unified Modelling Language;graph transformation;domainspecific modelling language semantics;

[13] 
Esther Guerra and Juan de Lara. Colouring: execution, debug and analysis of QVTrelations transformations through coloured petri nets. Software & Systems Modeling, 13(4):14471472, Oct 2014. [ bib  DOI ]
QVT is the standard language sponsored by the OMG to specify modeltomodel transformations. It includes three different languages, being QVTrelations (QVTR) the one with higherlevel of abstraction. Unfortunately, there is scarce tool support for it nowadays, with incompatibilities and disagreements between the few tools implementing it, and lacking support for the analysis and verification of transformations. Part of this situation is due to the fact that the standard provides only a semiformal semantics for QVTR. In order to alleviate this situation, this paper provides a semantics for QVTR through its compilation into coloured Petri nets. The theory of coloured Petri nets provides useful techniques to analyse transformations (e.g. detecting relation conflicts, or checking whether certain structures are generated or not in the target model) as well as to determine their confluence and termination given a starting model. Our semantics is flexible enough to permit the use of QVTR specifications not only for transformation and checkonly scenarios, but also for model matching and model comparison, not covered in the original standard. As a proof of concept, we report on the use of CPNTools for the execution, debugging, verification and validation of transformations, and on a tool chain (named Colouring) to transform QVTR specifications and their input models into the input format of CPNTools, as well as to export and visualize the transformation results back as models.

[14] 
Perdita Stevens. A simple gametheoretic approach to checkonly QVT relations. Software & Systems Modeling, 12(1):175199, Feb 2013. [ bib  DOI ]
The QVT Relations (QVTR) transformation language allows the definition of bidirectional model transformations, which are required in cases where two (or more) models must be kept consistent in the face of changes to either or both. A QVTR transformation can be used either in checkonly mode, to determine whether a target model is consistent with a given source model, or in enforce mode, to change the target model. A precise understanding of checkonly mode transformations is prerequisite to a precise understanding of enforce mode transformations, and this is the focus of this paper. In order to give semantics to checkonly QVTR transformations, we need to consider the overall structure of the transformation as given by when and where clauses, and the role of trace classes. In the standard, the semantics of QVTR are given both directly, and by means of a translation to QVT Core, a language which is intended to be simpler. In this paper, we argue that there are irreconcilable differences between the intended semantics of QVTR and those of QVT Core, so that no translation from QVTR to QVT Core can be semanticspreserving, and hence no such translation can be helpful in defining the semantics of QVTR. Treating QVTR directly, we propose a simple gametheoretic semantics. We demonstrate its behaviour on examples and show how it can be used to prove an example result comparing two QVTR transformations. We demonstrate that consistent models may not possess a single trace model whose objects can be read as traceability links in either direction. We briefly discuss the effect of variations in the rules of the game, to elucidate some design choices available to the designers of the QVTR language.

[15] 
Julian Bradfield and Perdita Stevens. Enforcing QVTR with muCalculus and Games. In Vittorio Cortellessa and Dániel Varró, editors, Fundamental Approaches to Software Engineering, pages 282296, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [ bib  DOI ]
QVTR is the standard Object Management Group bidirectional transformation language. In previous work, we gave a precise gametheoretic semantics for the checkonly semantics of QVTR transformations, including the recursive invocation of relations which is allowed and used, but not defined, by the QVT standard. In this paper, we take up the problem of enforce semantics, where the standard attempts formality, but at crucial points lapses into English. We show that our previous semantics can be extended to enforce mode, giving a precise semantics taking the standard into account.

[16] 
Daniel Calegari and Nora Szasz. Verification of model transformations: a survey of the stateoftheart. Electronic Notes In Theoretical Computer Science, 292:525, 2013. [ bib  DOI ] 
[17] 
M. Amrani, L. Lucio, G. Selim, B. Combemale, J. Dingel, H. Vangheluwe, Y. Le Traon, and J. R. Cordy. A tridimensional approach for studying the formal verification of model transformations. In 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pages 921928, April 2012. [ bib  DOI ]
Keywords: formal verification;tridimensional approach;formal verification;model transformation;model driven engineering;MDE;conforming model;Unified modeling language;Computational modeling;Semantics;Object oriented modeling;Syntactics;Analytical models;Educational institutions;Model Transformations;Verification;Classification;Properties;Formal Techniques

[18] 
N.A. Zafar. Formal specification and validation of railway network components using Z notation. IET Software, 3:312320(8), August 2009. [ bib  DOI ]
The railway interlocking system, being a safetycritical system, has achieved importance in the railway industry. Advanced technologies are being applied for its modelling, preventing collision and derailing of trains and at the same time allowing efficient movement of trains. In this study, we have applied Z notation by constructing a specification of the critical components of moving block interlocking. Graphs are used for modelling static components and are then integrated with Z to describe its entire state space. At first a real topology is transferred to a model topology in graph theory and then the critical components of the railway network, for example, tracks, switches, crossings and level crossing, are formalised. These components are integrated to define the static part of the system and then dynamic components, the state space of the static part, trains and controls, are integrated to describe the complete system. Formal specification of the system is given using Z and the model is analysed and validated using Z/EVES tool.
Keywords: formal specification;railway network component;graph theory;safetycritical system;state space;railway industry;model topology;formal validation;Znotation;

[19] 
Kobamelo Moremedi and John Andrew van der Poll. Transforming formal specification constructs into diagrammatic notations. In Alfredo Cuzzocrea and Sofian Maabout, editors, Model and Data Engineering, pages 212224, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [ bib  DOI ]
Specification plays a vital role in software engineering to facilitate the development of highly dependable software. Various techniques may be used for specification work. Z is a formal specification language that is based on a stronglytyped fragment of ZermeloFraenkel set theory and firstorder logic to provide for precise and unambiguous specifications. While diagrammatic specification languages may lack precision, they may, owing to their visual characteristics be a lucrative option for advocates of semiformal specification techniques. In this paper we investigate to what extent formal constructs, e.g. Z may be transformed into diagrammatic notations. Several diagrammatic notations are considered and combined for this purpose.

[20] 
Selma Djeddai, Martin Strecker, and Mohamed Mezghiche. Integrating a Formal Development for DSLs into Metamodeling. In Alberto Abelló, Ladjel Bellatreche, and Boualem Benatallah, editors, Model and Data Engineering, pages 5566, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. [ bib  DOI ]
Formal methods (such as interactive provers) are increasingly used in software engineering. They offer a formal frame that guarantees the correctness of developments. Nevertheless, they use complex notations that might be difficult to understand for unaccustomed users. On the contrary, visual specification languages use intuitive notations and allow to specify and understand software systems. Moreover, they permit to easily generate graphical interfaces or editors for Domain Specific Languages (DSLs) starting from a metamodel. However, they suffer from a lack of precise semantics. We are interested in combining these two complementary technologies by mapping the elements of the one into the other.

[21] 
Matthias Biehl. Literature study on model transformations. Royal Institute of Technology, Tech. Rep. ISRN/KTH/MMK, 2010. [ bib ] 
[22] 
Edgar Jakumeit, Sebastian Buchwald, Dennis Wagelaar, Li Dan, Ábel Hegedüs, Markus Herrmannsdörfer, Tassilo Horn, Elina Kalnina, Christian Krause, Kevin Lano, et al. A survey and comparison of transformation tools based on the transformation tool contest. Science of Computer Programming, 85:4199, 2014. [ bib  DOI ] 
[23] 
XML. https://www.omg.org/spec/xml/1.1/, Accessed 28 November 2019. [ bib ] 
[24] 
medini QVT. http://projects.ikv.de/qvt/wiki, Accessed 28 November 2019. [ bib ] 
[25] 
QVT. https://www.omg.org/spec/qvt/1.3/, Accessed 28 November 2019. [ bib ] 
[26] 
SmartQVT. https://sourceforge.net/projects/smartqvt, Accessed 19 July 2019. [ bib ] 
[27] 
JQVT. https://github.com/patins1/raas4emf, Accessed 19 July 2019. [ bib ] 
[28] 
Mark Saaltink. The Z/EVES system. In Jonathan P. Bowen, Michael G. Hinchey, and David Till, editors, ZUM 97: The Z Formal Specification Notation, pages 7285, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. [ bib  DOI ]
We describe the Z/EVES system, which allows Z specifications to be analysed in a number of different ways. Among the significant features of Z/EVES are domain checking, which ensures that a specification is meaningful, and a theorem prover that includes a decision procedure for simple arithmetic and a heuristic rewriting mechanism that recognizes “obvious” facts.

[29] 
ModelMorf. http://www.mdetools.com/detail.php?toolid=61, Accessed 19 July 2019. [ bib ] 
[30] 
Together. http://www.microfocus.com/products/requirementsmanagement/together/, Accessed 19 July 2019. [ bib ] 
[31] 
Dan Li, Xiaoshan Li, and Volker Stolz. QVTbased model transformation using XSLT. SIGSOFT Softw. Eng. Notes, 36(1):18, January 2011. [ bib  DOI ]
Keywords: QVT relations, XSLT, graphical notation, model transformations

[32] 
Christopher Gerking and Christian Heinzemann. Solving the Movie Database Case with QVTo. In CEUR Workshop Proceedings, volume 1305, pages 98102, 07 2014. [ bib ] 
[33] 
Nafiseh Kahani, Mojtaba Bagherzadeh, James R. Cordy, Juergen Dingel, and Daniel Varró. Survey and classification of model transformation tools. Software & Systems Modeling, Mar 2018. [ bib  DOI ]
Model transformation lies at the very core of modeldriven engineering, and a large number of model transformation languages and tools have been proposed over the last few years. These tools can be used to develop, transform, merge, exchange, compare, and verify models and metamodels. In this paper, we present a comprehensive catalog of existing metamodelbased transformation tools and compare them using a qualitative framework. We begin by organizing the 60 tools we identified into a general classification based on the transformation approach used. We then compare these tools using a number of particular facets, where each facet belongs to one of six different categories and may contain several attributes. The results of the study are discussed in detail and made publicly available in a companion website with a capability to search for tools using the specified facets as search criteria. Our study provides a thorough picture of the stateoftheart in model transformation techniques and tools. Our results are potentially beneficial to many stakeholders in the modeling community, including practitioners, researchers, and transformation tool developers.

[34] 
Andy Evans, Robert France, Kevin Lano, and Bernhard Rumpe. The uml as a formal modeling notation. In Jean Bézivin and PierreAlain Muller, editors, The Unified Modeling Language. UML'98: Beyond the Notation, pages 336348, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. [ bib  DOI ]
The Unified Modeling Language (UML) is rapidly emerging as a defacto standard for modelling OO systems. Given this role, it is imperative that the UML needs a welldefined, fully explored semantics. Such semantics is required in order to ensure that UML concepts are precisely stated and defined. In this paper we motivate an approach to formalizing UML in which formal specification techniques are used to gain insight into the semantics of UML notations and diagrams and describe a roadmap for this approach. The authors initiated the Precise UML (PUML) group in order to develop a precise semantic model for UML diagrams. The semantic model is to be used as the basis for a set of diagrammatical transformation rules, which enable formal deductions to be made about UML diagrams. A small example shows how these rules can be used to verify whether one class diagram is a valid deduction of another. Because these rules are presented at the diagrammatical level, it will be argued that UML can be successfully used as a formal modelling tool without the notational complexities that are commonly found in textual specification techniques.

[35] 
Artur Boronat and José Meseguer. An algebraic semantics for MOF. Formal Aspects of Computing, 22(3):269296, May 2010. [ bib  DOI ]
In modeldriven development, software artifacts are represented as models in order to improve productivity, quality, and cost effectiveness. In this area, the metaobject facility (MOF) standard plays a crucial role as a generic framework within which a wide range of modeling languages can be defined. The MOF standard aims at offering a good basis for modeldriven development, providing some of the building concepts that are needed: what is a model, what is a metamodel, what is reflection in the MOF framework, and so on. However, most of these concepts are not yet fully formally defined in the current MOF standard. In this paper we define a reflective, algebraic, executable framework for precise metamodeling based on membership equational logic (mel) that supports the MOF standard. Our framework provides a formal semantics of the following notions: metamodel, model, and conformance of a model to its metamodel. Furthermore, by using the Maude language, which directly supports mel specifications, this formal semantics is executable. This executable semantics has been integrated within the Eclipse modeling framework as a plugin tool called MOMENT2. In this way, formal analyses, such as semantic consistency checks, model checking of invariants and LTL model checking, become available within Eclipse to provide formal support for modeldriven development processes.

[36] 
Lijun Shan and Hong Zhu. A formal descriptive semantics of uml. In Shaoying Liu, Tom Maibaum, and Keijiro Araki, editors, Formal Methods and Software Engineering, pages 375396, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. [ bib  DOI ]
This paper proposes a novel approach to the formal definition of UML semantics. We distinguish descriptive semantics from functional semantics of modelling languages. The former defines which system is an instance of a model while the later defines the basic concepts underlying the models. In this paper, the descriptive semantics of class diagram, interaction diagram and state machine diagram are defined by first order logic formulas. A translation tool is implemented and integrated with the theorem prover SPASS to enable automated reasoning about models. The formalisation and reasoning of models is then applied to model consistency checking.

[37] 
KE Miloudi, YE Amrani, and A Ettouhami. An automated translation of UML class diagrams into a formal specification to detect UML inconsistencies. In The Sixth International Conference on Software Engineering Advances, ICSEA, pages 432438, Barcelona, Spain, October 2329 2011. [ bib ] 
[38] 
Petra Malik, Lindsay Groves, and Clare Lenihan. Translating Z to Alloy. In Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, and Steve Reeves, editors, Abstract State Machines, Alloy, B and Z, pages 377390, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. [ bib  DOI ]
Few tools are available to help with the difficult task of validating that a Z specification captures its intended meaning. One tool that has been proven to be useful for validating specifications is the Alloy Analyzer, an interactive tool for checking and visualising Alloy models. However, Z specifications need to be translated to Alloy notation to make use of the Alloy Analyzer. These translations have been performed manually so far, which is a cumbersome and errorprone activity. The aim of this paper is to explore to what extent this process can be automated.

[39] 
Leo Freitas, Jim Woodcock, and Zheng Fu. Posix file store in Z/Eves: an experiment in the verified software repository. Science of Computer Programming, 74(4):238257, 2009. [ bib  DOI ] 
[40] 
Regina Hebig, Christoph Seidl, Thorsten Berger, John Kook Pedersen, and Andrzej Wasowski. Model Transformation Languages Under a Magnifying Glass: A Controlled Experiment with Xtend, ATL, and QVT. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, pages 445455, New York, NY, USA, 2018. ACM. [ bib  DOI ]
Keywords: ATL, Experiment, Model Transformation Languages, QVT, Xtend

[41] 
Nuno Macedo and Alcino Cunha. Implementing QVTR bidirectional model transformations using Alloy. In Vittorio Cortellessa and Dániel Varró, editors, Fundamental Approaches to Software Engineering, pages 297311, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [ bib  DOI ]
QVT Relations (QVTR) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, in part due to ambiguities and omissions in the original semantics, acceptance and development of effective tool support has been slow. Recently, the checking semantics of QVTR has been clarified and formalized. In this paper we propose a QVTR tool that complies to such semantics. Unlike any other existing tool, it also supports metamodels enriched with OCL constraints (thus avoiding returning illformed models), and proposes an alternative enforcement semantics that works according to the simple and predictable “principle of least change”. The implementation is based on an embedding of both QVTR transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving.

[42] 
Julian Bradfield and Igor Walukiewicz. The mucalculus and Model Checking, pages 871919. Springer International Publishing, Cham, 2018. [ bib  DOI ]
This chapter presents that part of the theory of the μ$mu$calculus that is relevant to the modelchecking problem as broadly understood. The μ$mu$calculus is one of the most important logics in model checking. It is a logic with an exceptional balance between expressiveness and algorithmic properties.

[43] 
Kevin Lano. A compositional semantics of UMLRSDS. Software & Systems Modeling, 8(1):85116, Feb 2009. [ bib  DOI ]
This paper provides a semantics for the UMLRSDS (Reactive System Development Support) subset of UML, using the realtime action logic (RAL) formalism. We show how this semantics can be used to resolve some ambiguities and omissions in UML semantics, and to support reasoning about specifications using the B formal method and tools. We use `semantic profiles' to provide precise semantics for different semantic variation points of UML. We also show how RAL can be used to give a semantics to notations for realtime specification in UML. Unlike other approaches to UML semantics, which concentrate on the class diagram notation, our semantic representation has behaviour as a central element, and can be used to define semantics for use cases, state machines and interactions, in addition to class diagrams.

[44] 
Kevin Lano and Shekoufeh KolahdouzRahimi. Specification and verification of model transformations using umlrsds. In Dominique Méry and Stephan Merz, editors, Integrated Formal Methods, pages 199214, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. [ bib ]
In this paper we describe techniques for the specification and verification of model transformations using a combination of UML and formal methods. The use of UML 2 notations to specify model transformations facilitates the integration of model transformations with other software development processes. Extracts from three large case studies of the specification of model transformations are given, to demonstrate the practical application of the approach.

[45] 
Xiaoping Jia. An approach to animating Z specifications. pages 108113. Proceedings Nineteenth Annual International Computer Software and Applications Conference (COMPSAC'95), IEEE, 1995. [ bib  DOI ]
Keywords: formal specification;computer science education;specification languages;visual programming;computer aided software engineering;Z specifications;ZANS approach;animation approaches;imperative intermediate language;code synthesis;requirements validation;Z specification languages;Animation;Formal specifications;Specification languages;Input variables;Software engineering;Computer science;Information systems;Logic programming;Application software;Computer industry

[46] 
Kevin Lano, T. Clark, and S. KolahdouzRahimi. A framework for model transformation verification. Formal Aspects of Computing, 27(1):193235, Jan 2015. [ bib  DOI ]
A model transformation verification task may involve a number of different transformations, from one or more of a wide range of different model transformation languages, each transformation may have a particular transformation style, and there are a number of different verification properties which can be verified for each language and style of transformation. Transformations may operate upon many different modelling languages. This diversity of languages and properties indicates the need for a suitably generic framework for model transformation verification, independent of particular model transformation languages, and able to provide support for systematic procedures for verification across a range of languages, and for a range of properties. In this paper we describe the elements of such a framework, and apply this framework to some example transformation verification problems. The paper is novel in covering a wide range of different verification techniques for a wide range of MT languages, within an integrated framework.

[47] 
Joel Greenyer and Ekkart Kindler. Comparing relational model transformation technologies: implementing query/view/transformation with triple graph grammars. Software & Systems Modeling, 9(1):21, Jul 2009. [ bib  DOI ]
The Model Driven Architecture (MDA) is an approach to develop software based on different models. There are separate models for the business logic and for platform specific details. Moreover, code can be generated automatically from these models. This makes transforma tions a core technology for MDA and for modelbased software engineering approaches in general. Query/View/Transformation (QVT) is the transformation technology recently proposed for this purpose by the OMG. Triple Graph Grammars (TGGs) are another transformation technology proposed in the midnineties, used for example in the FUJABA CASE tool. In contrast to many other transformation technologies, both QVT and TGGs declaratively define the relation between two models. With this definition, a transformation engine can execute a transformation in either direction and, based on the same definition, can also propagate changes from one model to the other. In this paper, we compare the concepts of the declarative languages of QVT and TGGs. It turns out that TGGs and declarative QVT have many concepts in common. In fact, QVTCore can be mapped to TGGs. We show that QVTCore can be implemented by transforming QVTCore mappings to TGG rules, which can then be executed by a TGG transformation engine that performs the actual QVT transformation. Furthermore, we discuss an approach for mapping QVTRelations to TGGs. Based on the semantics of TGGs, we clarify semantic gaps that we identified in the declarative languages of QVT and, furthermore, we show how TGGs can benefit from the concepts of QVT.

[48] 
Joel Greenyer. A study of model transformation technologies: Reconciling TGGs with QVT. Master's thesis, University of Paderborn, 2006. [ bib ] 
[49] 
Esther Guerra and Juan de Lara. An algebraic semantics for qvtrelations checkonly transformations. Fundamenta Informaticae, 114(1):73101, 2012. [ bib  DOI ] 
[50] 
Edward D Willink. UMLX: A graphical transformation language for MDA. In 2nd OOPSLA Workshop on Generative Techniques in the context of Model Driven Architecture, 2003. [ bib ] 
[51] 
José Barranquero Tolosa, Oscar SanjuánMartínez, Vicente GarcíaDíaz, B Cristina Pelayo GBustelo, and Juan Manuel Cueva Lovelle. Towards the systematic measurement of ATL transformation models. Software: Practice and Experience, 41(7):789815, 2011. [ bib  DOI ]
Keywords: MDE, model, transformation, model, metatransformation, metrics, measurement

[52] 
Emine G. Aydal, Mark Utting, and Jim Woodcock. A comparison of statebased modelling tools for model validation. In Richard F. Paige and Bertrand Meyer, editors, Objects, Components, Models and Patterns, pages 278296, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. [ bib  DOI ]
In modelbased testing, one of the biggest decisions taken before modelling is the modelling language and the model analysis tool to be used to model the system under investigation. UML, Alloy and Z are examples of popular statebased modelling languages. In the literature, there has been research about the similarities and the differences between modelling languages. However, we believe that, in addition to recognising the expressive power of modelling languages, it is crucial to detect the capabilities and the weaknesses of analysis tools that parse and analyse models written in these languages. In order to explore this area, we have chosen four model analysis tools: USE, Alloy Analyzer, ZLive and ProZ and observed how modelling and validation stages of MBT are handled by these tools for the same system. Through this experiment, we not only concretise the tasks that form the modelling and validation stages of MBT process, but also reveal how efficiently these tasks are carried out in different tools.

[53] 
Ana Patrícia Fontes Magalhaes, Aline Maria Santos Andrade, and Rita Suzana Pitangueira Maciel. Model Driven Transformation Development (MDTD): An Approach for Developing Model to Model Transformation. Information and Software Technology, 114:5576, 2019. [ bib  DOI ] 
[54] 
Daniel Jackson. Software Abstractions: logic, language, and analysis. MIT press, 2012. [ bib ] 
[55] 
Sureyya Tarkan and Vibha Sazawal. Chief Chefs of Z to Alloy: Using a Kitchen Example to Teach Alloy with Z. In Jeremy Gibbons and José Nuno Oliveira, editors, Teaching Formal Methods, pages 7291, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. [ bib ]
Z is a welldefined and wellknown specification language. Unfortunately, it takes significant expertise to use existing tools (such as theorem provers) to automatically check properties of Z specifications. Because Alloy is substantially similar to Z and the Alloy Analyzer offers a relatively simple method of model checking, we believe that Alloy should be largely employed in classes that teach Z. To this end, we present an online tutorial especially designed to help students transition from Z to Alloy. The tutorial includes both the classic Birthday Book example and a large realworld scenario based on a Kitchen Environment. Our experiences with novices studying the tutorial suggest that the tutorial helps students learn both Z and Alloy. In addition, novices can answer questions correctly about the approximately 500line Kitchen Environment model after only a few hours of study.

[56] 
Daniel Jackson. Alloy: A Language and Tool for Exploring Software Designs. Commun. ACM, 62(9):6676, August 2019. [ bib  DOI  http ] 
[57] 
J. Bezivin, F. Jouault, and D. Touzet. Principles, standards and tools for model engineering. In 10th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'05), pages 2829, June 2005. [ bib  DOI ]
Keywords: formal specification;software architecture;software standards;software tools;standards;software tools;model engineering;AMMA;software architecture;eclipse modeling;conceptual architecture;Model driven engineering;DSL;Proposals;Automation;Bridges;Computer architecture;Production facilities;Domain specific languages;Acoustical engineering;Engineering management

[58] 
Bernhard Westfechtel. Casebased exploration of bidirectional transformations in QVT relations. Software & Systems Modeling, 17(3):9891029, 2018. [ bib ] 
[59] 
Bernhard Westfechtel and Thomas Buchmann. Incremental Bidirectional Transformations: Comparing Declarative and Procedural Approaches Using the Families to Persons Benchmark. In International Conference on Evaluation of Novel Approaches to Software Engineering, pages 98118. Springer, 2018. [ bib ] 
[60] 
Bernhard Westfechtel. Incremental bidirectional transformations: Applying qvt relations to the families to persons benchmark. In ENASE, pages 3953, 2018. [ bib ] 
