Abstract
The Query/View/Transformation Relations (QVT-R) standard for bidirectional model transformation is notorious for its underspecified semantics. When restricted to transformations between pairs of models, most of the ambiguities and omissions have been addressed in recent work. Nevertheless, the application of the QVT-R language is not restricted to that scenario, and similar issues remain unexplored for the multidirectional case (maintaining consistency between more than two models), that has been overlooked so far. In this paper we first discuss ambiguities and omissions in the QVT-R standard concerning the mutidirectional transformation scenario, and then propose a simple extension and formalization of the checking and enforcement semantics that clarifies some of them. We also discuss how such proposal could be implemented in our Echo bidirectional model transformation tool. Ours is just a small step towards making QVT-R a viable language for bidirectional transformation in realistic applications, and a considerable amount of basic research is still needed to fully accomplish that goal.

Abstract
Model finders are becoming useful in many software engineering problems. Kodkod [19] is one of the most popular, due to its support for relational logic (a combination of first order logic with relational algebra operators and transitive closure), allowing a simpler specification of constraints, and support for partial instances, allowing the specification of a priori (exact, but potentially partial) knowledge about a problem's solution. However, in some software engineering problems, such as model repair or bidirectional model transformation, knowledge about the solution is not exact, but instead there is a known target that the solution should approximate. In this paper we extend Kodkod's partial instances to allow the specification of such targets, and show how its model finding procedure can be adapted to support them (using both PMax-SAT solvers or SAT solvers with cardinality constraints). Two case studies are also presented, including a careful performance evaluation to assess the effectiveness of the proposed extension. © 2014 Springer-Verlag.

Abstract
Bidirectional transformation (BX) is a very active area of research interest. There is not only a growing body of theory, but also a rich set of tools supporting BX. The problem now arises that there is no commonly agreed-upon suite of tests or benchmarks that shows either the conformance of tools to theory, or the performance of tools in particular BX scenarios. This paper sets out to improve the state of affairs in this respect, by proposing a template and a set of required criteria for benchmark descriptions, as well as guidelines for the artifacts that should be provided for each included test. As a proof of concept, the paper additionally provides a detailed description of one concrete benchmark.

Abstract
Alloy is a formal modeling language based on first-order relational logic, with no native support for specifying reactive systems. We propose an extension of Alloy to allow the specification of temporal formulas using LTL, and show how they can be verified by bounded model checking with the Alloy Analyzer.

Abstract
Slicing is a distributed systems primitive that allows to autonomously partition a large set of nodes based on node-local attributes. Slicing is decisive for automatically provisioning system resources for different services, based on their requirements or importance. One of the main limitations of existing slicing protocols is that only single dimension attributes are considered for partitioning. In practical settings, it is often necessary to consider best compromises for an ensemble of metrics. In this paper we propose an extension of the slicing primitive that allows multi-attribute distributed systems slicing. Our protocol employs a gossip-based approach that does not require centralized knowledge and allows self-organization. It leverages the notion of domination between nodes, forming a partial order between multi-dimensional points, in a similar way to SkyLine queries for databases. We evaluate and demonstrate the interest of our approach using large-scale simulations.

Abstract
The ubiquity of data transformation problems in software engineering has led to the development of bidirectional transformation techniques in a variety of application domains. Model-driven engineering (MDE) is one of those areas, where such techniques are essential to maintain the consistency between multiple coexisting and simultaneously evolving models. However, the lack of in-depth research about certain characteristics of MDE has hindered the development of effective bidirectional model transformations that are able to address realistic MDE scenarios. This dissertation tackles two of these issues: that of constrained transformation domains and least-change transformations. The first regards the transformations’ ability to take into consideration the constraints imposed by the meta-models, and is essential to achieve correctness; the second regards the transformations’ ability to control the selection of updates from among those considered correct, and is essential to achieve a predictable system. These two issues are addressed under two popular bidirectional transformation schemes: in the context of the asymmetric framework of lenses, following a combinatorial approach; and in the context of the symmetric framework of constraint maintainers, proposing a solution based on model finding. The latter was effectively deployed as Echo, a tool for model repair and transformation. The expressiveness and flexibility provided by relational logic enabled it to be used as the unifying formalism throughout this dissertation.;A ubiquidade de problemas de transformação de dados em engenharia de software levou ao desenvolvimento de técnicas para transformação bidirecional numa variedade de domínios de aplicação. A Engenharia Baseada em Modelos (MDE) é uma dessas áreas, onde essas técnicas são essenciais para gerir a consistência entre múltiplos modelos que coexistem e evolvem simultaneamente. No entanto, a falta de estudos aprofundados sobre algumas características da MDE tem dificultado o desenvolvimento de técnicas de transformação bidirecional de modelos eficazes e que consigam lidar com cenários MDE realísticos. Esta dissertação aborda dois destes problemas: o de domínios de transformação restringidos e o de transformações com mudanças-mínimas. O primeiro tem que ver com a capacidade das transformações de ter em consideração as restrições impostas pelos meta-modelos e é essencial para atingir correcção; a segunda tem que ver com a capacidade de controlar a seleção de modificações entre as consideradas corretas, e é essencial para obter um sistema previsível. Esta tese aborda estes dois problemas sob dois populares esquemas de transformação bidirecional: no contexto da framework assimétrica das lentes, seguindo uma abordagem combinatorial, e no contexto da framework simétrica dos constraint maintainers, sendo proposta uma solução baseada em “procura de modelos”. Esta última foi efetivamente implementada como Echo, uma ferramenta para a reparação e transformação de modelos. A expressividade e flexibilidade proporcionada pela lógica relacional permitiu que esta fosse usada como o formalismo unificador desta dissertação.