Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Nuno Moreira Macedo
  • Cluster

    Informática
  • Cargo

    Investigador Sénior
  • Desde

    01 novembro 2011
004
Publicações

2022

Merging Cloned Alloy Models with Colorful Refactorings

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

Publicação
Science of Computer Programming

Abstract

2022

Schema-guided Testing of Message-oriented Systems

Autores
Santos, A; Cunha, A; Macedo, N;

Publicação
Proceedings of the 17th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2022, Online Streaming, April 25-26, 2022.

Abstract

2021

Experiences on teaching alloy with an automated assessment platform

Autores
Macedo, N; Cunha, A; Pereira, J; Carvalho, R; Silva, R; Paiva, ACR; Ramalho, MS; Silva, D;

Publicação
SCIENCE OF COMPUTER PROGRAMMING

Abstract

2021

The High-Assurance ROS Framework

Autores
Santos, A; Cunha, A; Macedo, N;

Publicação
3rd IEEE/ACM International Workshop on Robotics Software Engineering, RoSE@ICSE 2021, Madrid, Spain, June 2, 2021

Abstract

2020

Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum

Autores
Cunha, A; Macedo, N;

Publicação
Int. J. Softw. Tools Technol. Transf.

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.

Teses
supervisionadas

2021

Lightweight Trustworthy High-level Software Design

Autor
Chong Liu

Instituição
UM

2021

Graph databases for HR relationships

Autor
Rafael Araújo Moura

Instituição
UP-FEUP

2021

Safety Verification for ROS Applications

Autor
André Filipe Faria dos Santos

Instituição
UM

2020

Analysis of Message Passing Software Using Electrum

Autor
Bruno Renato Fernandes Carvalho

Instituição
UM

2019

Safety Verification for ROS Applications

Autor
André Filipe Faria dos Santos

Instituição
UM