Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
About

About

I'm currently a post-doctoral researcher at the HASLab unit of INESC TEC at the University of Minho, Portugal.

I've recently completed my joint PhD degree on computer science from the Universities of Minho, Aveiro and Porto, on a "Relational Approach to Bidirectional Transformation" under the supervision of Professor Alcino Cunha.

My research focuses on bridging the gap between formal methods and software engineering through the development of lightweight approaches and techniques, with the goal of improving the overall quality of software products. Current research topics include trustworthy software design frameworks and safety validation of robotic software.

Interest
Topics
Details

Details

  • Name

    Nuno Moreira Macedo
  • Cluster

    Computer Science
  • Role

    Researcher
  • Since

    01st November 2011
001
Publications

2017

A Feature-Based Classification of Model Repair Approaches

Authors
Macedo, N; Tiago, J; Cunha, A;

Publication
IEEE Trans. Software Eng.

Abstract
Consistency management, the ability to detect, diagnose and handle inconsistencies, is crucial during the development process in Model-driven Engineering (MDE). As the popularity and application scenarios of MDE expanded, a variety of different techniques were proposed to address these tasks in specific contexts. Of the various stages of consistency management, this work focuses on inconsistency handling in MDE, particularly in model repair techniques. This paper proposes a feature-based classification system for model repair techniques, based on an systematic literature review of the area. We expect this work to assist developers and researchers from different disciplines in comparing their work under a unifying framework, and aid MDE practitioners in selecting suitable model repair approaches. © 1976-2012 IEEE.

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.

2013

Implementing QVT-R Bidirectional Model Transformations Using Alloy

Authors
Macedo, N; Cunha, A;

Publication
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2013

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 has been slow. Recently, the checking semantics of QVT-R has been clarified and formalized. In this paper 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.

Supervised
thesis

2016

Safety Verification for ROS Applications

Author
André Filipe Faria dos Santos

Institution
UM

2016

A Web-based Social Environment for Alloy

Author
José Manuel Costa Pereira

Institution
UM

2016

Parallel verification of Dynamic Systems with Rich Configurations

Author
Eduardo Jose Dias Pessoa

Institution
UM

2015

Aplicação de Convenções de Código ao Robot Operating System

Author
André Filipe Faria dos Santos

Institution
UM

2015

Qualidade de Software para o Robot Operating System

Author
Miguel Ângelo Gomes da Costa

Institution
UM