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
2024 ACM/IEEE 44TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: SOFTWARE ENGINEERING EDUCATION AND TRAINING, ICSE-SEET 2024

Abstract
Background: Many progranunmg environments include automated feedback in the form of hints to help novices learn autonomously. Some experimental studies investigated the impact of automated liints 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

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.

2024

Alloy Goes Fuzzy

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

Publicação
RIGOROUS STATE-BASED METHODS, ABZ 2024

Abstract
Humans are good at understanding subjective or vague statements which, however, are hard to express in classical logic. Fuzzy logic is an evolution of classical logic that can cope with vague terms by handling degrees of truth and not just the crisp values true and false. Logic is the formal basis of computing, enabling the formal design of systems supported by tools such as model checkers and theorem provers.This paper shows how a model checker such as Alloy can evolve to handle both classical and fuzzy logic, enabling the specification of high-level quantitative relational models in the fuzzy domain. In particular, the paper showcases how QAlloy-F (a conservative, general-purpose quantitative extension to standard Alloy) can be used to tackle fuzzy problems, namely in the context of validating the design of fuzzy controllers. The evaluation of QAlloy-F against examples taken from various classes of fuzzy case studies shows the approach to be feasible.

2023

Task Model Design and Analysis with Alloy

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

Publicação
RIGOROUS STATE-BASED METHODS, ABZ 2023

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

Verifying Temporal Relational Models with Pardinus

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

Publicação
RIGOROUS STATE-BASED METHODS, ABZ 2023

Abstract
This short paper summarizes an article published in the Journal of Automated Reasoning [7]. It presents Pardinus, an extension of the popular Kodkod [12] relational model finder with linear temporal logic (including past operators) to simplify the analysis of dynamic systems. Pardinus 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.

Teses
supervisionadas

2023

Mining hints for fixing formal specifications

Autor
Henrique Gabriel dos Santos Neto

Instituição
UM

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

2022

Automatic Repair of Behavioural Specifications

Autor
Jorge Gabriel Alves Cerqueira

Instituição
UM

2022

Formalização da reconfiguração de protocolos de consenso usando Alloy

Autor
Cecília da Conceição de Oliveira Soares

Instituição
UM