Full contract verification for ATL using symbolic execution

The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the community that enhancing methods for exhaustively verifying such transformations allows for a more widespread adoption of model-driven engineering in industry. A variety of proposals for the verification of ATL transformations have arisen in the past few years. However, the majority of these techniques are either based on non-exhaustive testing or on proof methods that require human assistance and/or are not complete. In this paper, we describe our method for statically verifying the declarative subset of ATL model transformations. This verification is performed by translating the transformation (including features like filters, OCL expressions, and lazy rules) into our model transformation language DSLTrans. As we handle only the declarative portion of ATL, and DSLTrans is Turing-incomplete, this reduction in expressivity allows us to use a symbolic-execution approach to generate representations of all possible input models to the transformation. We then verify pre-/post-condition contracts on these representations, which in turn verifies the transformation itself. The technique we present in this paper is exhaustive for the subset of declarative ATL model transformations. This means that if the prover indicates a contract holds on a transformation, then the contract’s pre-/post-condition pair will be true for any input model for that transformation. We demonstrate and explore the applicability of our technique by studying several relatively large and complex ATL model transformations, including a model transformation developed in collaboration with our industrial partner. As well, we present our ‘slicing’ technique. This technique selects only those rules in the DSLTrans transformation needed for contract proof, thereby reducing proving time.     

From UML/SPT models to schedulability analysis: approach and a prototype implementation using ATL

Model Driven Architecture (MDA) is a software development approach promoted by the OMG. MDA is based on two key concepts, models and model transformations. Several kinds of models are generally used throughout the development process to specify a software system and to support its analysis and validation. UML and its extensions, such as the UML profile for real-time systems (UML/SPT), are commonly used to define the structure and the behavior of software systems while other models, such as performance models or schedulability models, are more suitable for performance or schedulability analysis, respectively. In this paper we discuss a model transformation enabling the derivation of schedulability analysis models from UML/SPT models. As a proof of concepts, we present a prototype implementation of this model transformation using ATL. We provide a definition of the source and target metamodels using the metamodel specification language KM3 and we specify the transformation in an ATL module. We discuss the merits and limitations of our approach and of its implementation.     

Contrasting dedicated model transformation languages versus general purpose languages: a historical perspective on ATL versus Java based on complexity and size

Model transformations are among the key concepts of model-driven engineering (MDE), and dedicated model transformation languages (MTLs) emerged with the popularity of the MDE pssaradigm about 15 to 20 years ago. MTLs claim to increase the ease of development of model transformations by abstracting from recurring transformation aspects and hiding complex semantics behind a simple and intuitive syntax. Nonetheless, MTLs are rarely adopted in practice, there is still no empirical evidence for the claim of easier development, and the argument of abstraction deserves a fresh look in the light of modern general purpose languages (GPLs) which have undergone a significant evolution in the last two decades. In this paper, we report about a study in which we compare the complexity and size of model transformations written in three different languages, namely (i) the Atlas Transformation Language (ATL), (ii) Java SE5 (2004–2009), and (iii) Java SE14 (2020); the Java transformations are derived from an ATL specification using a translation schema we developed for our study. In a nutshell, we found that some of the new features in Java SE14 compared to Java SE5 help to significantly reduce the complexity of transformations written in Java by as much as 45%. At the same time, however, the relative amount of complexity that stems from aspects that ATL can hide from the developer, which is about 40% of the total complexity, stays about the same. Furthermore we discovered that while transformation code in Java SE14 requires up to 25% less lines of code, the number of words written in both versions stays about the same. And while the written number of words stays about the same their distribution throughout the code changes significantly. Based on these results, we discuss the concrete advancements in newer Java versions. We also discuss to which extent new language advancements justify writing transformations in a general purpose language rather than a dedicated transformation language. We further indicate potential avenues for future research on the comparison of MTLs and GPLs in a model transformation context.

     

Module superimposition: a composition technique for rule-based model transformation languages

As the application of model transformation becomes increasingly commonplace, the focus is shifting from model transformation languages to the model transformations themselves. The properties of model transformations, such as scalability, maintainability and reusability, have become important. Composition of model transformations allows for the creation of smaller, maintainable and reusable transformation definitions that together perform a larger transformation. This paper focuses on composition for two rule-based model transformation languages: the ATLAS Transformation Language (ATL) and the QVT Relations language. We propose a composition technique called module superimposition that allows for extending and overriding rules in transformation modules. We provide executable semantics as well as a concise and scalable implementation of module superimposition based on ATL.     

Towards the systematic measurement of ATL transformation models

The Model‐Driven Engineering paradigm is aimed at raising the abstraction level of Software Engineering approaches through the systematic use of models as primary artifacts, not only in software design and development, but also to understand, interact, configure, and modify the runtime behavior of software. It tries to overcome the wall between the documentation and the real state of the implementation. For that matter, our long‐term goal seeks to reach a higher degree of interoperability among available meta‐modeling technologies through bridges among technological spaces (TS bridges). The proposed system provides several ATL (ATLAS Transformation Language) transformations that enable the application of measuring operations over ATL transformation models and rules, and the generation of different complementary end‐user models, such as SVG charts and (X)HTML reports. For this work, we have evaluated a set of meta‐modeling TS bridges among UML, MOF, Ecore, KM3, and Microsoft DSL Tools. These results provide quantitative measurements of the declarative and imperative constructs of these transformations and relative quality factors as well. In addition to this, all the top‐level results extracted from the measurement of these TS bridges are merged into one unique model in order to assist in performing a comparative study among them. This comparative study suggests that it is feasible to apply automatic transformations over transformation models, i.e. meta‐transformations. In this regard, there are many open research trends towards complete management, validation, optimization, and inference of TS bridges between complementary meta‐modeling technologies. Copyright © 2010 John Wiley & Sons, Ltd.     

Towards reusing hints from past fixes

With the usage of version control systems, many bug fixes have accumulated over the years. Researchers have proposed various automatic program repair (APR) approaches that reuse past fixes to fix new bugs. However, some fundamental questions, such as how new fixes overlap with old fixes, have not been investigated. Intuitively, the overlap between old and new fixes decides how APR approaches can construct new fixes with old ones. Based on this intuition, we systematically designed six overlap metrics, and performed an empirical study on 5,735 bug fixes to investigate the usefulness of past fixes when composing new fixes. For each bug fix, we created delta graphs (i.e., program dependency graphs for code changes), and identified how bug fixes overlap with each other in terms of the content, code structures, and identifier names of fixes. Our results show that if an APR approach knows all code name changes and composes new fixes by fully or partially reusing the content of past fixes, only 2.1% and 3.2% new fixes can be created from single or multiple past fixes in the same project, compared with 0.9% and 1.2% fixes created from past fixes across projects. However, if an APR approach knows all code name changes and composes new fixes by fully or partially reusing the code structures of past fixes, up to 41.3% and 29.7% new fixes can be created. By making the above observations and revealing other ten findings, we investigated the upper bound of reusable past fixes and composable new fixes, exploring the potential of existing and future APR approaches.     

An MDE-based method for bridging different design notations

Different communities have developed plenty of design notations for software engineering in support of practical (via UML) and rigorous (via formal methods) approaches. Hence the problem of bridging these notations rises. Model-driven engineering (MDE) is a new paradigm in software engineering, which treats models and model transformations as first class citizens. Furthermore, it is seen as a promising method for bridging heterogeneous platforms. In this paper, we provide an MDE-based approach to build bridges between informal, semi-formal and formal notations: Firstly, different notations are viewed as different domain specification languages (DSLs) and introduced into MDE, especially into the ATLAS Model Management Architecture (AMMA) platform, by metamodeling. Then, ATL transformation rules are built for semantics mapping. At last, TCS-based model-to-text syntax rules are developed, allowing one to map models to programs. Consequently, different design notations in both graphical style and grammatical style are bridged. A case study of bridging OMG SysML™ to LOTOS is also illustrated showing the validity and practicability of our approach.     

Towards certain fixes with editing rules and master data

A variety of integrity constraints have been studied for data cleaning. While these constraints can detect the presence of errors, they fall short of guiding us to correct the errors. Indeed, data repairing based on these constraints may not find certain fixes that are guaranteed correct, and worse still, may even introduce new errors when attempting to repair the data. We propose a method for finding certain fixes, based on master data, a notion of certain regions, and a class of editing rules. A certain region is a set of attributes that are assured correct by the users. Given a certain region and master data, editing rules tell us what attributes to fix and how to update them. We show how the method can be used in data monitoring and enrichment. We also develop techniques for reasoning about editing rules, to decide whether they lead to a unique fix and whether they are able to fix all the attributes in a tuple, relative to master data and a certain region. Furthermore, we present a framework and an algorithm to find certain fixes, by interacting with the users to ensure that one of the certain regions is correct. We experimentally verify the effectiveness and scalability of the algorithm.     

Formal foundation of consistent EMF model transformations by algebraic graph transformation

Model transformation is one of the key activities in model-driven software development. An increasingly popular technology to define modeling languages is provided by the Eclipse Modeling Framework (EMF). Several EMF model transformation approaches have been developed, focusing on different transformation aspects. To validate model transformations with respect to functional behavior and correctness, a formal foundation is needed. In this paper, we define consistent EMF model transformations as a restricted class of typed graph transformations using node type inheritance. Containment constraints of EMF model transformations are translated to a special kind of graph transformation rules such that their application leads to consistent transformation results only. Thus, consistent EMF model transformations behave like algebraic graph transformations and the rich theory of algebraic graph transformation can be applied to these EMF model transformations to show functional behavior and correctness. Furthermore, we propose parallel graph transformation as a suitable framework for modeling EMF model transformations with multi-object structures. Rules extended by multi-object structures can specify a flexible number of recurring structures. The actual number of recurring structures is dependent on the application context of such a rule. We illustrate our approach by selected refactorings of simplified statechart models. Finally, we discuss the implementation of our concepts in a tool environment for EMF model transformations.     

Definition and validation of model transformations

With model transformations becoming more widely used, there is an increasing need for approaches focussing on a systematic development of model transformations. Although a number of approaches for specifying model transformations exist, none of them focusses on systematically validating model transformations with respect to termination and confluence. Termination and confluence ensure that a model transformation always produces a unique result. Also called functionality, these properties are important requirements for practical applications of model transformations. In this paper, we introduce our approach to model transformation. Using and extending results from the theory of graph transformation, we investigate termination and confluence properties of model transformations specified in our approach. We establish a set of criteria for termination and confluence to be checked at design time by static analysis of the transformation rules and the underlying metamodels. Moreover, the criteria are formulated in such a way that they require less experience with the theory of graph transformation. Our concepts are illustrated by a running example of a model tranformation from statecharts to the process algebra Communicating Sequential Processes.     

Data Transformation in Cross-project Defect Prediction

Software metrics rarely follow a normal distribution. Therefore, software metrics are usually transformed prior to building a defect prediction model. To the best of our knowledge, the impact that the transformation has on cross-project defect prediction models has not been thoroughly explored. A cross-project model is built from one project and applied on another project. In this study, we investigate if cross-project defect prediction is affected by applying different transformations (i.e., log and rank transformations, as well as the Box-Cox transformation). The Box-Cox transformation subsumes log and other power transformations (e.g., square root), but has not been studied in the defect prediction literature. We propose an approach, namely Multiple Transformations (MT), to utilize multiple transformations for cross-project defect prediction. We further propose an enhanced approach MT+ to use the parameter of the Box-Cox transformation to determine the most appropriate training project for each target project. Our experiments are conducted upon three publicly available data sets (i.e., AEEEM, ReLink, and PROMISE). Comparing to the random forest model built solely using the log transformation, our MT+ approach improves the F-measure by 7, 59 and 43% for the three data sets, respectively. As a summary, our major contributions are three-fold: 1) conduct an empirical study on the impact that data transformation has on cross-project defect prediction models; 2) propose an approach to utilize the various information retained by applying different transformation methods; and 3) propose an unsupervised approach to select the most appropriate training project for each target project.     

Slicing ATL model transformations for scalable deductive verification and fault localization

Model-driven engineering (MDE) is increasingly accepted in industry as an effective approach for managing the full life cycle of software development. In MDE, software models are manipulated, evolved and translated by model transformations (MT), up to code generation. Automatic deductive verification techniques have been proposed to guarantee that transformations satisfy correctness requirements (encoded as transformation contracts). However, to be transferable to industry, these techniques need to be scalable and provide the user with easily accessible feedback. In MT-specific languages like ATL, we are able to infer static trace information (i.e., mappings among types of generated elements and rules that potentially generate these types). In this paper, we show that this information can be used to decompose the MT contract and, for each sub-contract, slice the MT to the only rules that may be responsible for fulfilling it. Based on this contribution, we design a fault localization approach for MT, and a technique to significantly enhance scalability when verifying large MTs against a large number of contracts. We implement both these algorithms as extensions of the VeriATL verification system, and we show by experimentation that they increase its industry readiness.     

Towards language-to-language transformation

This paper proposes a simplicity-oriented approach and framework for language-to-language transformation of, in particular, graphical languages. Key to simplicity is the decomposition of the transformation specification into sub-rule systems that separately specify purpose-specific aspects. We illustrate this approach by employing a variation of Plotkin’s Structural Operational Semantics (SOS) for pattern-based transformations of typed graphs in order to address the aspect ‘computation’ in a graph rewriting fashion. Key to our approach are two generalizations of Plotkin’s structural rules: the use of graph patterns as the matching concept in the rules, and the introduction of node and edge types. Types do not only allow one to easily distinguish between different kinds of dependencies, like control, data, and priority, but may also be used to define a hierarchical layering structure. The resulting Type-based Structural Operational Semantics (TSOS) supports a well-structured and intuitive specification and realization of semantically involved language-to-language transformations adequate for the generation of purpose-specific views or input formats for certain tools, like, e.g., model checkers. A comparison with the general-purpose transformation frameworks ATL and Groove, illustrates along the educational setting of our graphical WebStory language that TSOS provides quite a flexible format for the definition of a family of purpose-specific transformation languages that are easy to use and come with clear guarantees.

     

A Matrix-Based Approach to Global Locality Optimization

Global locality optimization is a technique for improving the cache performance of a sequence of loop nests through a combination of loop and data layout transformations. Pure loop transformations are restricted by data dependencies and may not be very successful in optimizing imperfectly nested loops and explicitly parallelized programs. Although pure data transformations are not constrained by data dependencies, the impact of a data transformation on an array might be program-wide; that is, it can affect all the references to that array in all the loop nests. Therefore, in this paper we argue for an integrated approach that employs both loop and data transformations. The method enjoys the advantages of most of the previous techniques for enhancing locality and is efficient. In our approach, the loop nests in a program are processed one by one and the data layout constraints obtained from one nest are propagated for optimizing the remaining loop nests. We show a simple and effective matrix-based framework to implement this process. The search space that we consider for possible loop transformations can be represented by general nonsingular linear transformation matrices and the data layouts that we consider are those that can be expressed using hyperplanes. Experiments with several floating-point programs on an 8-processor SGI Origin 2000 distributed-shared-memory machine demonstrate the efficacy of our approach.     

Towards the efficient development of model transformations using model weaving and matching transformations

Model transformations can be used in many different application scenarios, for instance, to provide interoperability between models of different size and complexity. As a consequence, they are becoming more and more complex. However, model transformations are typically developed manually. Several code patterns are implemented repetitively, thus increasing the probability of programming errors and reducing code reusability. There is not yet a complete solution that automates the development of model transformations. In this paper, we present a novel approach that uses matching transformations and weaving models to semi-automate the development of transformations. Weaving models are models that contain different kinds of relationships between model elements. These relationships capture different transformation patterns. Matching transformations are a special kind of transformations that implement methods that create weaving models. We present a practical solution that enables the creation and the customization of different creation methods in an efficient way. We combine different methods, and present a metamodel-based method that exploits metamodel data to automatically produce weaving models. The weaving models are derived into model integration transformations. To validate our approach, we present an experiment using metamodels with distinct size and complexity, which show the feasibility and scalability of our solution.

一种结合MDA的高阶模型转换方法

模型转换是MDA的关键技术,也是MDA的研究热点。目前,不同的MDA开发平台都有一套相对独立的开发技术和转换框架,这使平台之间缺乏兼容性,模型转换代码重用困难。究其原因是缺少一种与具体转换语言相对应,且与平台无关的转换规则模型。为了解决以上问题,将高阶模型转换的思想与模型驱动软件开发相结合,提出了一种构造模型转换规则的高阶转换元模型,并以ATL语言为例展示了高阶转换元模型的使用方法;最后通过一个实例验证了该方法的可行性和可用性。该方法提高了模型转换语言的抽象层次,降低了模型转换语言的重用难度,在一定程度上解决了模型转换技术不兼容的问题。     

交互式数据清理系统的研究

当今数据清理方案需要反复进行数据质量分析以查找错误，为修复它们而进行的转换需要运行很长的时间。用户需要忍受长时间的等待，而且经常需要撰写复杂的转换脚本。我们所探讨的交互式数据清理系统，它能紧密地将转换和偏差检测集成在一起，只要发现偏差，用户就可以交互式地使用简单的图表操作、实例描述逐渐建立一个转换，无需书写复杂的程序或忍受很长的延时。     

Foundations for Streaming Model Transformations by Complex Event Processing

Streaming model transformations represent a novel class of transformations to manipulate models whose elements are continuously produced or modified in high volume and with rapid rate of change. Executing streaming transformations requires efficient techniques to recognize activated transformation rules over a live model and a potentially infinite stream of events. In this paper, we propose foundations of streaming model transformations by innovatively integrating incremental model query, complex event processing (CEP) and reactive (event-driven) transformation techniques. Complex event processing allows to identify relevant patterns and sequences of events over an event stream. Our approach enables event streams to include model change events which are automatically and continuously populated by incremental model queries. Furthermore, a reactive rule engine carries out transformations on identified complex event patterns. We provide an integrated domain-specific language with precise semantics for capturing complex event patterns and streaming transformations together with an execution engine, all of which is now part of the Viatra reactive transformation framework. We demonstrate the feasibility of our approach with two case studies: one in an advanced model engineering workflow; and one in the context of on-the-fly gesture recognition.     

Adapting transformations to metamodel changes via external transformation composition

Evolution is inherent to software systemsbecause of the rapid improvement of technologies and business logic. As a software development paradigm, model driven engineering (MDE) is also affected by this problem. More concretely, being metamodels the cornerstone of MDE, their evolution impacts the rest of software artefacts involved in a development process, i.e., models and transformations. The influence over models has been tackled and partially solved in previous works. This paper focuses on the impact over transformations. We propose an approach to adapt transformations by means of external transformation composition. That is, we chain impacted transformations to particular adaptation transformations which deal with either refactoring/destruction changes or construction changes. Our approach semi-automatically generates such transformations by using the AtlanMod matching language, a DSL to define model matching strategies. To provide with a proof of concept for our proposal, we adapt transformations written in terms of object-relational database metamodels when such metamodels evolve in time.     

From model transformation to incremental bidirectional model synchronization

The model-driven software development paradigm requires that appropriate model transformations are applicable in different stages of the development process. The transformations have to consistently propagate changes between the different involved models and thus ensure a proper model synchronization. However, most approaches today do not fully support the requirements for model synchronization and focus only on classical one-way batch-oriented transformations. In this paper, we present our approach for an incremental model transformation which supports model synchronization. Our approach employs the visual, formal, and bidirectional transformation technique of triple graph grammars. Using this declarative specification formalism, we focus on the efficient execution of the transformation rules and how to achieve an incremental model transformation for synchronization purposes. We present an evaluation of our approach and demonstrate that due to the speedup for the incremental processing in the average case even larger models can be tackled.