Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by HASLab

2016

Electronic governance in Portugal: a silent pioneer

Authors
Fernandes, Sara; Barbosa, LuisSoares;

Publication
Proceedings of the International Conference on Electronic Governance and Open Society - Challenges in Eurasia, EGOSE 2016, St. Petersburg, Russia, November 22-23, 2016

Abstract

2016

Electronic governance in Portugal

Authors
Fernandes, S; Barbosa, LS;

Publication
Proceedings of the International Conference on Electronic Governance and Open Society Challenges in Eurasia - EGOSE '16

Abstract

2016

A Framework for Quality Assessment of ROS Repositories

Authors
Santos, A; Cunha, A; Macedo, N; Lourenco, C;

Publication
2016 IEEE/RSJ INTERNATIONAL CONFERENCE ON INTELLIGENT ROBOTS AND SYSTEMS (IROS 2016)

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.

2016

Least-change bidirectional model transformation with QVT-R and ATL

Authors
Macedo, N; Cunha, A;

Publication
SOFTWARE AND SYSTEMS MODELING

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.

2016

Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations

Authors
Macedo, N; Brunel, J; Chemouil, D; Cunha, A; Kuperberg, D;

Publication
FSE'16: PROCEEDINGS OF THE 2016 24TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON FOUNDATIONS OF SOFTWARE ENGINEERING

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.

2016

Alloy meets TLA+: An exploratory study

Authors
Macedo, N; Cunha, A;

Publication
CoRR

Abstract

  • 126
  • 261