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

Alcino Cunha é Professor Associado no Departamento de Informático da Universidade do Minho e membro (e atualmente co-coordenador) do Laboratório de Software Confiável, um centro de investigação do laboratório associado INESC TEC. A sua investigação tem por ambição tornar o desenvolvimento formal de software mais acessível para todos os engenheiros de software, tendo sido um dos proponentes da nova versão 6 do acessível método formal Alloy, que adicionou suporte para especificações comportamentais e lógica temporal. Também tem interesse no tópico da qualidade de software robótico, em particular no desenvolvimento de ferramentas de análise formal para software desenvolvido com o popular framework ROS. Publicou mais de 70 artigos, incluindo vários artigos em revistas e conferências relevantes na área da engenharia de software e da robótica, tais como TSE, FSE, ASE, IROS, ou FM. 

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Alcino Cunha
  • Cargo

    Coordenador de Centro
  • Desde

    01 novembro 2011
003
Publicações

2024

Assessing the impact of hints in learning formal specification

Autores
Cunha, A; Macedo, N; Campos, JC; Margolis, I; Sousa, E;

Publicação
Proceedings of the 46th International Conference on Software Engineering: Software Engineering Education and Training, SEET@ICSE 2024, Lisbon, Portugal, April 14-20, 2024

Abstract
Background: Many programming environments include automated feedback in the form of hints to help novices learn autonomously. Some experimental studies investigated the impact of automated hints in the immediate performance and learning retention in that context. Automated feedback is also becoming a popular research topic in the context of formal specification languages, but so far no experimental studies have been conducted to assess its impact while learning such languages. Objective: We aim to investigate the impact of different types of automated hints while learning a formal specification language, not only in terms of immediate performance and learning retention, but also in the emotional response of the students. Method: We conducted a simple one-factor randomised experiment in 2 sessions involving 85 BSc students majoring in CSE. In the 1st session students were divided in 1 control group and 3 experimental groups, each receiving a different type of hint while learning to specify simple requirements with the Alloy formal specification language. To assess the impact of hints on learning retention, in the 2nd session, 1 week later, students had no hints while formalising requirements. Before and after each session the students answered a standard self-reporting emotional survey to assess their emotional response to the experiment. Results: Of the 3 types of hints considered, only those pointing to the precise location of an error had a positive impact on the immediate performance and none had significant impact in learning retention. Hint availability also causes a significant impact on the emotional response, but no significant emotional impact exists once hints are no longer available (i.e. no deprivation effects were detected). Conclusion: Although none of the evaluated hints had an impact on learning retention, learning a formal specification language with an environment that provides hints with precise error locations seems to contribute to a better overall experience without apparent drawbacks. Further studies are needed to investigate if other kind of feedback, namely hints combined with some sort of self-explanation prompts, can have a positive impact in learning retention. © 2024 Copyright held by the owner/author(s).

2024

Validating multiple variants of an automotive light system with Alloy 6

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

Publicação
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER

Abstract
This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Alloy and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants.

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

An Experimental Evaluation of Tools for Grading Concurrent Programming Exercises

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

Publicação
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

Teses
supervisionadas

2023

Mining hints for fixing formal specifications

Autor
Henrique Gabriel dos Santos Neto

Instituição
UM

2023

Formalização de um protocolo Mesh para sistemas IoT em Alloy

Autor
Rafael Inácio Lourenço

Instituição
UM

2022

An HAROS extension for Variability Aware ROS Code Analysis

Autor
Ricardo Ribeiro Pereira

Instituição
UP-FCUP

2022

Codificação e análise de grafos de computação ROS variacionais

Autor
Pedro Rafael Paiva Moura

Instituição
UM

2022

Formalizing ROS2 security configuration with Alloy

Autor
Luís Mário Macedo Ribeiro

Instituição
UM