While most model-transformation languages in Model-Driven Engineering are unidirectional, bidirectionality is valuable when artifacts need two-way synchronization. Although several bidirectional transformation engines have been developed, their behavior is generally considered more difficult to formulate and predict compared to the unidirectional case. In the bidirectionalization approach, users write the forward direction of their transformations in the same unidirectional language they are used to, and obtain a system that (besides performing the complete forward transformation) can automatically propagate in the backward direction the target updates. When possible, full bidirectionalization is desirable, but far from trivial.

Some areas in computer science are characterized by a shared base structure for data artifacts (e.g., list, table, tree, graph, model), and dedicated languages for transforming this structure. We observe that in several of these languages it is possible to identify a clear correspondence between some elements in the transformation code and the output they generate. Conversely given an element in an output artifact it is often possible to immediately trace the transformation parts that are responsible for its creation. In this paper we formalize this intuitive concept by defining a property that characterizes several transformation languages in different domains. We name this property additivity: for a given fixed input, the addition or removal of program elements results in a corresponding addition or removal of parts of the output. We provide a formal definition for additivity and argue that additivity enhances modularity and incrementality of transformation engineering activities, by enumerating a set of tasks that this property enables or facilitates. Then we describe how it is instantiated in some well-known transformation languages. We expect that the development of new formal results on languages with additivity will benefit from our definitions.

This paper solves the known problem of elimination of unnecessary internal element construction as well as variable elimination in XML processing with (a subset of) XQuery without ignoring the issues of document order. The semantics of XQuery is context sensitive and requires preservation of document order. In this paper, we propose, as far as we are aware, the first XQuery fusion that can deal with both the document order and the context of XQuery expressions. More specifically, we carefully design a context representation of XQuery expressions based on the Dewey order encoding, develop a context-preserving XQuery fusion for ordered trees by static emulation of the XML store, and prove that our fusion is correct. Our XQuery fusion has been implemented, and all the examples in this paper have passed through the system.

Abstract: In model-Driven development (MDD), metamodels, models, and model transformations are interdependent. A change in one artifact must be reflected in all other related artifacts. Regardless of their dependencies, (meta)models and transformations can evolve autonomously rendering referenced artifacts invalid. Coupling the evolution of models to their corresponding metamodels tries to prevent such mismatches, but is currently limited to one-way adaptations and does not take model transformations into account. To eliminate these short-comings, we combine first-class transformation models with bidirectional transformations (BX). Our generic approach integrates BX into well-established Eclipse-based MDD tools, thereby neither being restricted to a specific modeling nor model transformation language. 1

Structural recursion, in the form of, for example, folds on lists and catamorphisms on algebraic data structures including trees, plays an important role in functional programming, by providing a systematic way for constructing and manipulating functional programs. It is, however, a challenge to define structural recursions for graph data structures, the most ubiquitous sort of data in computing. This is because unlike lists and trees, graphs are essentially not inductive and cannot be formalized as an initial algebra in general. In this paper, we borrow from the database community the idea of structural recursion on how to restrict recursions on infinite unordered regular trees so that they preserve the finiteness property and become terminating, which are desirable properties for query languages. We propose a new graph transformation language called lambdaFG for transforming and querying ordered graphs, based on the well-defined bisimulation relation on ordered graphs with special epsilon-edges. The language lambdaFG is a higher order graph transformation language that extends the simply typed lambda calculus with graph constructors and more powerful structural recursions, which is extended for transformations on the sibling dimension. It not only gives a general framework for manipulating graphs and reasoning about them, but also provides a solution to the open problem of how to define a structural recursion on ordered graphs, with the help of the bisimilarity for ordered graphs with epsilon-edges.

We introduce a lambda calculus λTFG for transformations of finite graphs by generalizing and extending an existing calculus UnCAL. Whereas UnCAL can treat only unordered graphs, λTFG can treat a variety of graph models: directed edge-labeled graphs whose branch styles are represented by monads T. For example, λTFG can treat unordered graphs, ordered graphs, weighted graphs, probability graphs, and so on, by using the powerset monad, list monad, multiset monad, probability monad, respectively. In λTFG, graphs are considered as extension of tree data structures, i.e. as infinite (regular) trees, so the semantics is given with bisimilarity.

We propose OptIQ, a query optimization approach for iterative queries in distributed environment. OptIQ removes redundant computations among different iterations by extending the traditional techniques of view materialization and incremental view evaluation. First, OptIQ decomposes iterative queries into invariant and variant views, and materializes the former view. Redundant computations are removed by reusing the materialized view among iterations. Second, OptIQ incrementally evaluates the variant view, so that redundant computations are removed by skipping the evaluation on converged tuples in the variant view. We verify the effectiveness of OptIQ through the queries of PageRank and k-means clustering on real datasets. The results show that OptIQ achieves high efficiency, up to five times faster than is possible without removing the redundant computations among iterations.

Following the “convention over configuration” paradigm, model-driven development (MDD) generates code to implement the “default” behaviour that has been specified by a template separate from the input model, reducing the decision effort of developers. For flexibility, users of MDD are allowed to customise the model and the generated code in parallel. A synchronisation of changed model or code is maintained by reflecting them on the other end of the code generation, as long as the traceability is unchanged. However, such invariant traceability between corresponding model and code elements can be violated either when (a) users of MDD protect custom changes from the generated code, or when (b) developers of MDD change the template for generating the default behaviour. A mismatch between user and template code is inevitable as they evolve for their own purposes. In this paper, we propose a two-layered invariant traceability framework that reduces the number of mismatches through bidirectional transformations. On top of existing vertical (model↔code) synchronisations between a model and the template code, a horizontal (code↔code) synchronisation between user and template code is supported, aligning the changes in both directions. Our blinkit tool is evaluated using the data set available from the CVS repositories of a MDD project: Eclipse MDT/GMF.

Bidirectional model transformation is useful for maintaining consistency between two models, and has many potential applications in software development including model synchronization, round-trip engineering, and software evolution. Despite these attractive uses, the lack of a practical tool support for systematic development of well-behaved and efficient bidirectional model transformation prevents it from being widely used. In this paper, we solve this problem by proposing an integrated framework called GRoundTram, which is carefully designed and implemented for compositional development of well-behaved and efficient bidirectional model transformations. GRoundTram is built upon a well-founded bidirectional framework, and is equipped with a user-friendly language for coding bidirectional model transformation, a new tool for validating both models and bidirectional model transformations, an optimization mechanism for improving efficiency, and a powerful debugging environment for testing bidirectional behavior. GRoundTram has been used by people of other groups and their results show its usefulness in practice.

This paper presents a new approach to solving the problem of verification of graph transformation, by proposing a new static verification algorithm for the Core UnCAL, the query algebra for graph-structured databases proposed by Bunemann et al. Given a graph transformation annotated with schema information, our algorithm statically verifies that any graph satisfying the input schema is converted by the transformation to a graph satisfying the output schema. We tackle the problem by first reformulating the semantics of UnCAL into monadic second-order logic (MSO). The logic-based foundation allows to express the schema satisfaction of transformations as the validity of MSO formulas over graph structures. Then by exploiting the two established properties of UnCAL called bisimulation-genericity and compactness, we reduce the problem to the validity of MSO over trees, which has a sound and complete decision procedure. The algorithm has been efficiently implemented; all the graph transformations in this paper and the system web page can be verified within several seconds.

Bidirectional transformations provide a novel mechanism for syn-chronizing and maintaining the consistency of information between input and output. Despite many promising results on bidirectional transformations, these have been limited to the context of relational or XML (tree-like) databases. We challenge the problem of bidirec-tional transformations within the context of graphs, by proposing a formal definition of a well-behaved bidirectional semantics for UnCAL, i.e., a graph algebra for the known UnQL graph query language. The key to our successful formalization is full utiliza-tion of both the recursive and bulk semantics of structural recur-sion on graphs. We carefully refine the existing forward evaluation of structural recursion so that it can produce sufficient trace infor-mation for later backward evaluation. We use the trace information for backward evaluation to reflect in-place updates and deletions on the view to the source, and adopt the universal resolving algorithm for inverse computation and the narrowing technique to tackle the difficult problem with insertion. We prove our bidirectional evalu-ation is well-behaved. Our current implementation is available on-line and confirms the usefulness of our approach with nontrivial applications.