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
Sobre

Sobre

Sou professor auxiliar no Departamento de Engenharia Informática (DEI) da Faculdade de Engenharia da Universidade do Porto (FEUP), Portugal, e investigador sénior no HASLab, a unidade do INESC TEC focada do desenvolvimento de software confiável, onde desenvolvo, ensino e aplico técnicas formais à engenharia de software.


A minha investigação foca-se na concepção de software confiável, particularmente na aplicação de técnicas formais "lightweight" à concepção de software baseadas em "model check" e "model finding". Faço parte da equipa que mantém o Alloy 6 e o seu Analyzer, uma ferramenta para analisar modelos de software. Adaptei também esse tipo de técnicas ao domínio da robótica para promover o desenvolvimento de software robótico confiável, assim como é projetos de transferência de conhecimento e de consultadoria.


As minhas atividades letivas focam-se no ensino de linguagens de programação e de métodos formais na engenharia de software. Nesse contexto, mantenho também o Alloy4Fun, uma plataforma para apoiar o ensino de Alloy.

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Nuno Moreira Macedo
  • Cargo

    Investigador Sénior
  • Desde

    01 novembro 2011
003
Publicações

2023

Task Model Design and Analysis with Alloy

Autores
Cunha, A; Macedo, N; Kang, E;

Publicação
Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings

Abstract
This paper describes a methodology for task model design and analysis using the Alloy Analyzer, a formal, declarative modeling tool. Our methodology leverages (1) a formalization of the HAMSTERS task modeling notation in Alloy and (2) a method for encoding a concrete task model and compose it with a model of the interactive system. The Analyzer then automatically verifies the overall model against desired properties, revealing counter-examples (if any) in terms of interaction scenarios between the operator and the system. In addition, we demonstrate how Alloy can be used to encode various types of operator errors (e.g., inserting or omitting an action) into the base HAMSTERS model and generate erroneous interaction scenarios. Our methodology is applied to a task model describing the interaction of a traffic air controller with a semi-autonomous Arrival MANager (AMAN) planning tool. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

2023

Verifying Temporal Relational Models with Pardinus

Autores
Macedo, N; Brunel, J; Chemouil, D; Cunha, A;

Publicação
Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings

Abstract
This short paper summarizes an article published in the Journal of Automated Reasoning [7]. It presents, an extension of the popular [12] relational model finder with linear temporal logic (including past operators) to simplify the analysis of dynamic systems. includes a SAT-based bounded model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counterexamples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

2023

Adding Records to Alloy

Autores
Brunel, J; Chemouil, D; Cunha, A; Macedo, N;

Publicação
Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings

Abstract
Records are a composite data type available in most programming and specification languages, but they are not natively supported by Alloy. As a consequence, users often find themselves having to simulate records in ad hoc ways, a strategy that is error prone and often encumbers the analysis procedures. This paper proposes a conservative extension to the Alloy language to support record signatures. Uniqueness and completeness is imposed on the atoms of such signatures, while still supporting Alloy’s flexible signature hierarchy. The Analyzer has been extended to internally expand such record signatures as partial knowledge for the solving procedure. Evaluation shows that the proposed approach is more efficient than commonly used idioms. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

2023

Exploring Automatic Specification Repair in Dafny Programs

Autores
Abreu, A; Macedo, N; Mendes, A;

Publicação
2023 38TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING WORKSHOPS, ASEW

Abstract
Formal verification has become increasingly crucial in ensuring the accurate and secure functioning of modern software systems. Given a specification of the desired behaviour, i.e. a contract, a program is considered to be correct when all possible executions guarantee the specification. Should the software fail to behave as expected, then a bug is present. Most existing research assumes that the bug is present in the implementation, but it is also often the case that the specified expectations are incorrect, meaning that it is the specification that must be repaired. Research and tools for providing alternative specifications that fix details missing during contract definition, considering that the implementation is correct, are scarce. This paper presents a preliminary tool, focused on Dafny programs, for automatic specification repair in contract programming. Given a Dafny program that fails to verify, the tool suggests corrections that repair the specification. Our approach is inspired by a technique previously proposed for another contract programming language and relies on Daikon for dynamic invariant inference. Although the tool is focused on Dafny, it makes use of specification repair techniques that are generally applicable to programming languages that support contracts. Such a tool can be valuable in various scenarios, such as when programmers have a reference implementation and need to analyse their contract options, or in educational contexts, where it can provide students with hints to correct their contracts. The results of the evaluation show that the approach is feasible in Dafny and that the overall process has reasonable performance but that there are stages of the process that need further improvements.

2022

Merging cloned Alloy models with colorful refactorings

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

Publicação
SCIENCE OF COMPUTER PROGRAMMING

Abstract
Likewise to code, clone-and-own is a common way to create variants of a model, to explore the impact of different features while exploring the design of a software system. Previously, we have introduced Colorful Alloy, an extension of the popular Alloy language and toolkit to support feature-oriented design, where model elements can be annotated with feature expressions and further highlighted with different colors to ease understanding. In this paper we propose a catalog of refactoring laws for Colorful Alloy models, and show how they can be used to iteratively merge cloned Alloy models into a single featureannotated colorful model, where the commonalities and differences between the different clones are easily perceived, and more efficient aggregated analyses can be performed. We then show how these refactorings can be composed in an automated merging strategy that can be used to migrate Alloy clones into a Colorful Alloy SPL in a single step. The paper extends a conference version [1] by formalizing the semantics and type system of the improved Colorful Alloy language, allowing the simplification of some rules and the evaluation of their soundness. Additional rules were added to the catalog, and the evaluation extended. The automated merging strategy is also novel.

Teses
supervisionadas

2021

Graph databases for HR relationships

Autor
Rafael Araújo Moura

Instituição
UP-FEUP

2021

Lightweight Trustworthy High-level Software Design

Autor
Chong Liu

Instituição
UM

2020

Radio-Frequency Based Location Service

Autor
João Filipe Lopes de Carvalho

Instituição
UP-FEUP

2020

Interactive multimodal and procedurally-assisted creation of VR environments

Autor
João Pedro Martins Ferreira

Instituição
UP-FEUP

2020

Life Bracelet

Autor
Tiago Miguel Delgadinho Simões

Instituição
UP-FEUP