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 am assistant professor at the Department of Informatics of Universidade do Minho, where I regularly teach courses on programming and formal methods for software engineering, and also a member of the High-Assurance Software Laboratory of INESC TEC. In recent years, my research is focused on the topic of formal methods for software engineering, namely developing new languages and tools for formal modeling, including validatiom and verificaiton, and for bidirectional model transformation. Recently, I've also started to research the topic of robotic software quality, in particular software developed for the Robot Operating System.

Interest
Topics
Details

Details

  • Name

    Alcino Cunha
  • Cluster

    Computer Science
  • Role

    Centre Coordinator
  • Since

    01st November 2011
006
Publications

2022

Merging Cloned Alloy Models with Colorful Refactorings

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

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract

2022

Merging Cloned Alloy Models with Colorful Refactorings

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

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract

2022

Schema-guided Testing of Message-oriented Systems

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

Publication
ENASE: PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING

Abstract
Effective testing of message-oriented software requires describing the expected behaviour of the system and the causality relations between messages. This is often achieved with formal specifications based on temporal logics that require both first-order and metric temporal constructs - to specify constraints over data and real time. This paper proposes a technique to automatically generate tests for metric first-order temporal specifications that match well-understood specification patterns. Our approach takes in properties in a high-level specification language and identifies test schemas (strategies) that are likely to falsify the property. Schemas correspond to abstract classes of execution traces, that can be refined by introducing assumptions about the system. At the low level, concrete traces are successively produced for each schema using property-based testing principles. We instantiate this approach for a popular robotic middleware, ROS, and evaluate it on two systems, showing that schema-based test generation is effective for message-oriented software.

2022

Timely Specification Repair for Alloy 6

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

Publication
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2022

Abstract

2022

Quantitative relational modelling with QAlloy

Authors
Silva, P; Oliveira, JN; Macedo, N; Cunha, A;

Publication
Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18, 2022

Abstract

Supervised
thesis

2021

Lightweight Trustworthy High-level Software Design

Author
Chong Liu

Institution
UM

2021

Safety Verification for ROS Applications

Author
André Filipe Faria dos Santos

Institution
UM

2021

Interpretabilidade em Aprendizagem Máquina num Contexto de Modelos de Regressão Caixa Negra

Author
João Pedro Torres Pimentel

Institution
UM

2020

Safety Verification for ROS Applications

Author
André Filipe Faria dos Santos

Institution
UM

2020

Lightweight Trustworthy High-level Software Design

Author
Chong Liu

Institution
UM