Abstract

Abstract
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 have been slow. Recently, the checking semantics of QVT-R has been clarified and formalized. In this article, 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. We also show how this technique can be applied to bidirectionalize ATL, a popular (but unidirectional) model transformation language.

Abstract
Model-checking is increasingly popular in the early phases of the software development process. To establish the correctness of a software design one must usually verify both structural and behavioral(or temporal) properties. Unfortunately, most specification languages, and accompanying model-checkers, excel only in analyzing either one or the other kind. This limits their ability to verify dynamic systems with rich configurations: systems whose state space is characterized by rich structural properties, but whose evolution is also expected to satisfy certain temporal properties. To address this problem, we first propose Electrum, an extension of the Alloy specification language with temporal logic operators, where both rich configurations and expressive temporal properties can easily be de fined. Two alternative model-checking techniques are then proposed, one bounded and the other unbounded, to verify systems expressed in this language, namely to verify that every desirable temporal property holds for every possible configuration.

Abstract
Buffer caching mechanisms are paramount to improve the performance of today's massive scale NoSQL databases. In this work, we show that in fact there is a direct and univocal relationship between the resource usage and the cache hit ratio in NoSQL databases. In addition, this relationship can be leveraged to build a mechanism that is able to estimate resource usage of the nodes composing the NoSQL cluster.

Abstract
In the last three decades with the Information Technologies advent and the growth of the concept of Virtual Environments, a set of new ways to perform tasks have emerged, in the most diversified areas of society. The main focus of this work was to verify if it was possible to increase the sense of presence through multi-sensory stimulation, creating a virtual environment of simulation that causes stress in exposure therapy, in this case in people who have a fear of heights. The evaluation of the sense of presence was made using the Portuguese version of a previously validated IPQ (Igroup Presence Questionnaire) and also through direct observation of the movements caused by oculomotor reflexes. Although the achievement results that were not very significant between the two tested groups, the multisensory simulation environment obtained better results in terms of involvement in relation to space and realism, which increased concentration in the experience. The obtained results seem to indicate that the alone addition of further stimuli does not lead to an increased feeling of presence, therefore existing the need to understand which are the critical stimuli for each assessment situation.

Abstract
Currently, a learning management system (LMS) plays a central role in any e-learning environment. These environments include systems to handle the pedagogic aspects of the teaching-learning process (e.g. specialized tutors, simulation games) and the academic aspects (e.g. academic management systems). Thus, the potential for interoperability is an important, although over looked, aspect of an LMS. In this paper, we make a comparative study of the interoperability level of the most relevant LMS. We start by defining an application and a specification model. For the application model, we create a basic application that acts as a tool provider for LMS integration. The specification model acts as the API that the LMS should implement to communicate with the tool provider. Based on researches, we select the Learning Tools Interoperability (LTI) from IMS. Finally, we compare the LMS interoperability level defined as the effort made to integrate the application on the study LMS.