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
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

    Senior Researcher
  • Since

    01st November 2011
003
Publications

2020

Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum

Authors
Cunha, A; Macedo, N;

Publication
International Journal on Software Tools for Technology Transfer

Abstract
This paper reports on the development of a formal model for the Hybrid ERTMS/ETCS Level 3 concept in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic operators. We show how Electrum and its Analyzer can be used to perform scenario exploration to validate this model, namely to check that all the operational scenarios described in the reference document are admissible, and to reason about expected safety properties, which can be easily specified and model checked for arbitrary track configurations. We also show how the Analyzer can be used to depict scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable by stakeholders without expertise in formal specification. © 2019, Springer-Verlag GmbH Germany, part of Springer Nature.

2020

Validating Multiple Variants of an Automotive Light System with Electrum

Authors
Cunha, A; Macedo, N; Liu, C;

Publication
Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings

Abstract

2020

Experiences on Teaching Alloy with an Automated Assessment Platform

Authors
Macedo, N; Cunha, A; Pereira, J; Carvalho, R; Silva, R; Paiva, ACR; Ramalho, MS; Silva, DC;

Publication
Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings

Abstract

2020

Merging Cloned Alloy Models with Colorful Refactorings

Authors
Liu, C; Macedo, N; Cunha, A;

Publication
Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings

Abstract

2020

ROSY: An elegant language to teach the pure reactive nature of robot programming

Authors
Pacheco, H; Macedo, N;

Publication
Fourth IEEE International Conference on Robotic Computing, IRC 2020, Taichung, Taiwan, November 9-11, 2020

Abstract
Robotics is very appealing and is long recognized as a great way to teach programming, while drawing inspiring connections to other branches of engineering and science such as maths, physics or electronics. Although this symbiotic relationship between robotics and programming is perceived as largely beneficial, educational approaches often feel the need to hide the underlying complexity of the robotic system, but as a result fail to transmit the reactive essence of robot programming to the roboticists and programmers of the future. This paper presents ROSY, a novel language for teaching novice programmers through robotics. Its functional style is both familiar with a high-school algebra background and a materialization of the inherent reactive nature of robotic programming. Working at a higher-level of abstraction also teaches valuable design principles of decomposition of robotics software into collections of interacting controllers. Despite its simplicity, ROSY is completely valid Haskell code compatible with the ROS ecosystem. We make a convincing case for our language by demonstrating how non-trivial applications can be expressed with ease and clarity, exposing its sound functional programming foundations, and developing a web-enabled robot programming environment. © 2020 IEEE.

Supervised
thesis

2020

Analysis of Message Passing Software Using Electrum

Author
Bruno Renato Fernandes Carvalho

Institution
UM

2019

Safety Verification for ROS Applications

Author
André Filipe Faria dos Santos

Institution
INESCTEC

2019

Aplicação de Técnicas de Análise Formal a Software Robótico

Author
Gonçalo Nuno Esteves Duarte

Institution
UM

2019

Lightweight Trustworthy High-level Software Design

Author
Chong Liu

Institution
INESCTEC

2018

Safety Verification for ROS Applications

Author
André Filipe Faria dos Santos

Institution
UM