Abstract

Abstract
Robots are being increasingly used in safety-critical contexts, such as transportation and health. The need for flexible behavior in these contexts, due to human interaction factors or unstructured operating environments, led to a transition from hardware-to software-based safety mechanisms in robotic systems, whose reliability and quality is imperative to guarantee. Source code static analysis is a key component in formal software verification. It consists on inspecting code, often using automated tools, to determine a set of relevant properties that are known to influence the occurrence of defects in the final product. This paper presents HAROS, a generic, plug-in-driven, framework to evaluate code quality, through static analysis, in the context of the Robot Operating System (ROS), one of the most widely used robotic middleware. This tool (equipped with plug-ins for computing metrics and conformance to coding standards) was applied to several publicly available ROS repositories, whose results are also reported in the paper, thus providing a first overview of the internal quality of the software being developed in this community.

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

Abstract
On-line applications and services are now a critical part of our everyday life. Using these services typically requires us to trust our personal or company's information to a large number of third-party entities. These entities enforce several security measures to avoid unauthorized accesses but data is still stored on common database systems that are designed without data privacy concerns in mind. As a result, data is vulnerable against anyone with direct access to the database, which may be external attackers, malicious insiders, spies or even subpoenas. Building strong data privacy mechanisms on top of common database systems is possible but has a significant impact on the system's resources, computational capabilities and performance. Notably, the amount of useful computation that may be done over strongly encrypted data is close to none, which defeats the purpose of offloading computation to third-party services. In this paper, we propose to shift the need to trust in the honesty and security of service providers to simply trust that they will not collude. This is reasonable as cloud providers, being competitors, do not share data among themselves. We focus on NoSQL databases and present SafeRegions, a novel prototype of a distributed and secure NoSQL database that is built on top of HBase and that guarantees strong data privacy while still providing most of HBase's query capabilities. SafeRegions relies on secret sharing and multiparty computation techniques to provide a NoSQL database built on top of multiple, non-colluding service providers that appear as a single one to the user. Strikingly, service providers, individually, cannot disclose any of the user's data but, together, are able to offer data storage and processing capabilities. Additionally, we evaluate SafeRegions exposing performance trade-offs imposed by security mechanisms and provide useful insights for future research on performance optimization.