Formalizing the main characteristics of QVT-based model transformation languages

Document Type: Research Article

Authors

1 Faculty of Information Technology and Computer Engineering, Azarbaijan Shahid Madani University, Tabriz, Iran.

2 Department of Informatics, King's College London, London, UK.

10.22108/jcs.2020.121740.1047

Abstract

Model-Driven Development (MDD) aims at developing software more productively by using models as the main artifacts. Here, the models with high abstraction levels must be transformed into lower levels and finally executable models, i.e., source code. As a result, model transformation languages/tools play a main role on realizing the MDD goal. The Object-Management Group (OMG) presented the Query/View/Transformation (QVT) as a standard for the Meta-Object Facility (MOF)-based model transformation languages.
However, implementing a model transformation language, which supports the full features of the QVT proposal requires a formal model of the underlying concepts. Having common terminology and a formal, precise, and consistent specification facilitates developing dependable transformation languages/tools.
This paper aims to provide a formal specification of the main characteristics of a QVT-Relations (QVTr) model transformation language using the Z notation. The proposed formal model can be adapted for formalizing other domain and language concepts too. To show the applicability of the proposed formalism, a simplified version of the classic object-relational transformation is specified. Additionally, we show how the semantics clarifies some outstanding semantic issues in QVTr. The proposed formalism of this paper will pave the way to building support tools for model transformations in a unified manner in MDD.

Keywords

Main Subjects


[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):555--577, Jul 2013. [ bib | DOI ]
Model transformation is one of the pillars of model-driven 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 principles---just like any other kind of software---there 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 429--433, 2005. [ bib | DOI ]
[3] Soon-Kyeong Kim, David Carrington, and Roger Duke. A metamodel-based transformation between UML and Object-Z. In Proceedings IEEE Symposia on Human-Centric Computing Languages and Environments (Cat. No.01TH8587), pages 112--119. Proceedings IEEE Symposia on Human-Centric Computing Languages and Environments (Cat. No.01TH8587), Sep. 2001. [ bib | DOI ]
Keywords: specification languages;object-oriented languages;visual languages;metamodel-based transformation;UML;Object-Z;formal modeling notations;visual modeling notations;software models;imprecise incomplete inconsistent transformation task;meta-level 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):289--295, 2011. [ bib ]
[5] Jim Woodcock and Jim Davies. Using Z: specification, refinement, and proof. Prentice-Hall, 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):31--39, 2008. [ bib | DOI ]
[7] Dan Li, Xiaoshan Li, and Volker Stolz. QVT-based Model Transformation Using XSLT. SIGSOFT Softw. Eng. Notes, 36(1):1--8, 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):171--188, 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, model-integrated 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 code-centric to model-based 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 class-based 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:69--81, 2006. [ bib | DOI ]
[10] Nuno Amálio and Fiona Polack. Comparison of formalisation approaches of uml class constructs in Z and Object-Z. In Didier Bert, Jonathan P. Bowen, Steve King, and Marina Waldén, editors, ZB 2003: Formal Specification and Development in Z and B, pages 339--358, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. [ bib | DOI ]
UML, and other object-oriented 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 Object-Z approaches to object-oriented formalisation. The Z approaches reflect different formalisation goals (a formal model of the system, a formal model of a diagrammatic object-oriented model). The Object-Z 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. Addison-Wesley Professional, 2003. [ bib ]
[12] C. Amelunxen. Formalising model transformation rules for UML/MOF 2. IET Software, 2:204--222(18), June 2008. [ bib | DOI ]
Model-driven software development, today's state-of-the-art approach to the design of software, can be applied in various domains and thus demands a variety of domain-specific modelling languages. The specification of a domain-specific 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 non-trivial 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: domain-specific modelling language syntax;meta object facility 2;object constraint language;model-driven software development;UML;Unified Modelling Language;graph transformation;domain-specific modelling language semantics;
[13] Esther Guerra and Juan de Lara. Colouring: execution, debug and analysis of QVT-relations transformations through coloured petri nets. Software & Systems Modeling, 13(4):1447--1472, Oct 2014. [ bib | DOI ]
QVT is the standard language sponsored by the OMG to specify model-to-model transformations. It includes three different languages, being QVT-relations (QVT-R) the one with higher-level 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 semi-formal semantics for QVT-R. In order to alleviate this situation, this paper provides a semantics for QVT-R 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 QVT-R specifications not only for transformation and check-only 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 QVT-R 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 game-theoretic approach to checkonly QVT relations. Software & Systems Modeling, 12(1):175--199, Feb 2013. [ bib | DOI ]
The QVT Relations (QVT-R) 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 QVT-R 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 QVT-R 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 QVT-R 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 QVT-R and those of QVT Core, so that no translation from QVT-R to QVT Core can be semantics-preserving, and hence no such translation can be helpful in defining the semantics of QVT-R. Treating QVT-R directly, we propose a simple game-theoretic semantics. We demonstrate its behaviour on examples and show how it can be used to prove an example result comparing two QVT-R 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 QVT-R language.
 
[15] Julian Bradfield and Perdita Stevens. Enforcing QVT-R with mu-Calculus and Games. In Vittorio Cortellessa and Dániel Varró, editors, Fundamental Approaches to Software Engineering, pages 282--296, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [ bib | DOI ]
QVT-R is the standard Object Management Group bidirectional transformation language. In previous work, we gave a precise game-theoretic semantics for the checkonly semantics of QVT-R 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 state-of-the-art. Electronic Notes In Theoretical Computer Science, 292:5--25, 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 921--928, 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:312--320(8), August 2009. [ bib | DOI ]
The railway interlocking system, being a safety-critical 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;safety-critical system;state space;railway industry;model topology;formal validation;Z-notation;
[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 212--224, 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 strongly-typed fragment of Zermelo-Fraenkel set theory and first-order 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 semi-formal 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 Meta-modeling. In Alberto Abelló, Ladjel Bellatreche, and Boualem Benatallah, editors, Model and Data Engineering, pages 55--66, 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 meta-model. 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:41--99, 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 72--85, 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/requirements-management/together/, Accessed 19 July 2019. [ bib ]
[31] Dan Li, Xiaoshan Li, and Volker Stolz. QVT-based model transformation using XSLT. SIGSOFT Softw. Eng. Notes, 36(1):1--8, 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 98--102, 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 model-driven 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 metamodel-based 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 state-of-the-art 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 Pierre-Alain Muller, editors, The Unified Modeling Language. UML'98: Beyond the Notation, pages 336--348, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. [ bib | DOI ]
The Unified Modeling Language (UML) is rapidly emerging as a de-facto standard for modelling OO systems. Given this role, it is imperative that the UML needs a well-defined, 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):269--296, May 2010. [ bib | DOI ]
In model-driven development, software artifacts are represented as models in order to improve productivity, quality, and cost effectiveness. In this area, the meta-object 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 model-driven 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 model-driven 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 375--396, 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 432--438, Barcelona, Spain, October 23-29 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 377--390, 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 error-prone 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):238--257, 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 445--455, New York, NY, USA, 2018. ACM. [ bib | DOI ]
Keywords: ATL, Experiment, Model Transformation Languages, QVT, Xtend
[41] Nuno Macedo and Alcino Cunha. Implementing QVT-R bidirectional model transformations using Alloy. In Vittorio Cortellessa and Dániel Varró, editors, Fundamental Approaches to Software Engineering, pages 297--311, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [ bib | DOI ]
QVT Relations (QVT-R) 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 QVT-R has been clarified and formalized. In this paper we propose a QVT-R tool that complies to such semantics. Unlike any other existing tool, it also supports meta-models enriched with OCL constraints (thus avoiding returning ill-formed 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 QVT-R 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 mu-calculus and Model Checking, pages 871--919. Springer International Publishing, Cham, 2018. [ bib | DOI ]
This chapter presents that part of the theory of the μ$mu$-calculus that is relevant to the model-checking 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 UML-RSDS. Software & Systems Modeling, 8(1):85--116, Feb 2009. [ bib | DOI ]
This paper provides a semantics for the UML-RSDS (Reactive System Development Support) subset of UML, using the real-time 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 real-time 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 Kolahdouz-Rahimi. Specification and verification of model transformations using uml-rsds. In Dominique Méry and Stephan Merz, editors, Integrated Formal Methods, pages 199--214, 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 108--113. 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. Kolahdouz-Rahimi. A framework for model transformation verification. Formal Aspects of Computing, 27(1):193--235, 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 model-based 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 mid-nineties, 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, QVT-Core can be mapped to TGGs. We show that QVT-Core can be implemented by transforming QVT-Core 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 QVT-Relations 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 qvt-relations check-only transformations. Fundamenta Informaticae, 114(1):73--101, 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án-Martínez, Vicente García-Díaz, B Cristina Pelayo G-Bustelo, and Juan Manuel Cueva Lovelle. Towards the systematic measurement of ATL transformation models. Software: Practice and Experience, 41(7):789--815, 2011. [ bib | DOI ]
Keywords: MDE, model, transformation, model, meta-transformation, metrics, measurement
[52] Emine G. Aydal, Mark Utting, and Jim Woodcock. A comparison of state-based modelling tools for model validation. In Richard F. Paige and Bertrand Meyer, editors, Objects, Components, Models and Patterns, pages 278--296, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. [ bib | DOI ]
In model-based 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 state-based 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:55--76, 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 72--91, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. [ bib ]
Z is a well-defined and well-known 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 real-world 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 500-line 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):66--76, 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 28--29, 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. Case-based exploration of bidirectional transformations in QVT relations. Software & Systems Modeling, 17(3):989--1029, 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 98--118. Springer, 2018. [ bib ]
[60] Bernhard Westfechtel. Incremental bidirectional transformations: Applying qvt relations to the families to persons benchmark. In ENASE, pages 39--53, 2018. [ bib ]