Abstract
Model-driven engineering (MDE) is a software engineering approach based on model transformations at different abstraction levels. It prescribes the development of software by successively transforming the models from abstract (specifications) to more concrete ones (code). Alloy is an increasingly popular lightweight formal specification language that supports automatic verification. Unfortunately, its widespread industrial adoption is hampered by the lack of an ecosystem of MDE tools, namely code generators. This paper presents a model transformation from Alloy to UML class diagrams annotated with OCL (UML+OCL) and shows how an existing transformation from UML+OCL to Alloy can be improved to handle dynamic issues. The proposed bidirectional transformation enables a smooth integration of Alloy in the current MDE contexts, by allowing UML+OCL specifications to be transformed to Alloy for validation and verification, to correct and possibly refine them inside Alloy, and to translate them back to UML+OCL for sharing with stakeholders or to reuse current model-driven architecture tools to refine them toward code.

Abstract
Three-dimensional virtual worlds (3DVW) have been growing fast in number of users, and are used for the most diverse purposes. In collaboration, 3DVW are used with good results due to features such as immersion, interaction capabilities, use of avatar embodiment, and physical space. In the particular cases of avatar embodiment and physical space, these features support nonverbal communication, but its impact on collaboration is not well known. In this work we present the initial steps for creation of a protocol for case study research, aiming to assert itself as a tool to collect data on how nonverbal communication influences collaboration in 3DVW. We define the propositions and units of analysis, and a pilot case to validate them.

Abstract
The problem of homing a mobile robot to a given reference location under unknown relative and absolute positions is addressed in this paper. This problem is easy to solve when all the positions and kinematic variables are known or are observable, but remains a challenge when only range is measured. Its complexity further increases when variable and unknown drifts are added to the motion, which is typical for marine vehicles. Based on the range measurements, it is possible to drive the robot arbitrarily close to the reference. This paper presents a complete solution and demonstrates the validity of the approach based on the Lyapunov theory. The use of models, which are often affected by uncertainties and/or unmodeled terms, is intended to be minimal and only some constraints are imposed on the speed of the robot. We derive a control law that makes the robot converge asymptotically to the reference and prove its stability theoretically. Nevertheless, as it is well known, practical limitations on the actuation can weaken some properties of convergence, namely when the system dynamics require increasing actuation along the approach trajectory. We will demonstrate that the robot reaches a positively invariant set around the reference whose upper bound is determined. Finally, we conclude our work by presenting simulation and experimental data and by demonstrating the validity and the robustness of the method.

Abstract

Abstract

Abstract