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

    Centre Coordinator
  • Since

    01st November 2011
003
Publications

2023

Task Model Design and Analysis with Alloy

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

Publication
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

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

Publication
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

An Experimental Evaluation of Tools for Grading Concurrent Programming Exercises

Authors
Barros, M; Ramos, M; Gomes, A; Cunha, A; Pereira, J; Almeida, PS;

Publication
Formal Techniques for Distributed Objects, Components, and Systems - 43rd IFIP WG 6.1 International Conference, FORTE 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings

Abstract

2023

Adding Records to Alloy

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

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

2022

Merging cloned Alloy models with colorful refactorings

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

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

Supervised
thesis

2021

Providing Flexibility in Distribution Systems by Electric Vehicles and Distributed Energy Resources in the Context of Technical Virtual Power Plants

Author
Pedro Miguel de Carvalho Pereira

Institution
UP-FEUP

2021

Lightweight Trustworthy High-level Software Design

Author
Chong Liu

Institution
UM

2020

Life Bracelet

Author
Tiago Miguel Delgadinho Simões

Institution
UP-FEUP

2020

Radio-Frequency Based Location Service

Author
João Filipe Lopes de Carvalho

Institution
UP-FEUP

2020

Interactive multimodal and procedurally-assisted creation of VR environments

Author
João Pedro Martins Ferreira

Institution
UP-FEUP