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.

Abstract

Abstract
Today E-Government institutions face a lot of challenges related to the quality and effectiveness of the services they provide. In most cases, their users are more demanding, imposing new ways of acting and dealing with their needs, requesting often expeditious and effective attendance. Independently for their nature, we believe that such pertinent characteristics begin to be sustained immediately as we start to study and model E-Government processes. Modeling and simulation are useful tools on the assurance of the availability of E-Government services in many aspects, contributing significantly to improve processes implementation, ranging from their inception to their final software application roll-up and maintenance. In this paper we studied the use of YAWL - a work flowing language - for modeling E-Government processes, showing through a real world application case how it can help us in the construction of effective models that may be used as a basis for understanding and building the correspondent software applications. Copyright 2014 ACM.

Abstract
Model synchronization plays an important role in modeldriven software development. Bidirectional model transformation approaches provide techniques for developers to specify the bidirectional relationship between source and target models, while keeping related models synchronized for free. Since models of interest are usually not in a one-to-one correspondence, this synchronization process is inherently ambiguous. Nevertheless, existing bidirectional model transformation tools focus mainly on enforcing consistency and provide developers only limited control over how models are synchronized, solving the latent ambiguity via default strategies whose behavior is unclear to developers. In this paper, we propose a novel approach in which developers write update programs that succinctly describe how a target model can be used to update a source model, such that the bidirectional behavior is fully determined. The new approach mitigates the unpredictability of existing solutions, by enabling a finer and more transparent control of what a bidirectional transformation does, and suggests a research direction for building more robust bidirectional model transformation tools. Copyright © 2014 ACM.