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
Publicações

2025

Does Every Computer Scientist Need to Know Formal Methods?

Autores
Broy, M; Brucker, AD; Fantechi, A; Gleirscher, M; Havelund, K; Kuppe, MA; Mendes, A; Platzer, A; Ringert, JO; Sullivan, A;

Publicação
Formal Aspects Comput.

Abstract
We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence "While there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career."We argue that formal methods are and have to be an integral part of every computer science curriculum. Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently. The same way, students have to understand why and how formal methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these.In this article, we aim at highlighting why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students' programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program design and justification, rather than simply writing programs without reflection and deeper understanding. Since integrating formal methods into the computer science curriculum is not a straightforward process, we explore the additional question: what are the tradeoffs between one dedicated knowledge area of formal methods in a computer science curriculum versus having formal methods scattered across all knowledge areas? Solving problems while designing software and software-intensive systems demands an understanding of what is required, followed by a specification and formalizing a solution in a programming language. How to do this systematically and correctly on solid grounds is exactly supported by formal methods. © 2024 Copyright held by the owner/author(s).

2025

Enhancing Recruitment with LLMs and Chatbots

Autores
Liliana Novais; Vitor Rocio; Jorge Morais;

Publicação
Distributed Computing and Artificial Intelligence, Special Sessions II, 21st International Conference

Abstract

2025

Comparative analysis of EU-based cybersecurity skills frameworks

Autores
Almeida, F;

Publicação
Computers & Security

Abstract

2025

Collaborative Fault Tolerance for Cyber-Physical Systems: The Diagnosis Stage

Autores
Piardi, L; Costa, P; De Oliveira, AS; Leitao, P;

Publicação
IEEE Access

Abstract
The reliability and robustness of cyber-physical systems (CPS) are critical aspects of the current industrial landscape. The high level of autonomous and distributed components associated with a large number of devices makes CPS prone to faults. Despite their importance and benefits, traditional fault tolerance methodologies, namely local and/or centralized, often overlook the potential benefits of collaboration between cyber-physical components. This paper introduces a collaborative fault diagnosis methodology for CPS, integrating self-fault diagnosis capabilities in agents and leveraging collaborative behavior to enhance fault diagnosis. The contribution of this paper relay in propose a methodology for fault diagnosis for CPS, based on multi-agent system (MAS) technology as a backbone of infra-structure, highlighting the components, agent behavior, functionalities, and interaction protocols, to explore the benefits of communication and collaboration between agents. The proposed methodology enhance the accuracy of fault diagnosis when compared with local approach. A case study was conducted in a laboratory-scale warehouse, focusing on diagnosing drift, bias, and precision faults in temperature and humidity sensors. Experimental results reveal that the collaborative methodology significantly outperforms the local approach in fault diagnosis, as evidenced by performance improvements in diagnosis classification. The statistical significance of these results was validated using the Wilcoxon signed-ranks test for paired samples. © 2013 IEEE.

2025

Automated optical system for quality inspection on reflective parts

Autores
Nascimento, R; Rocha, CD; Gonzalez, DG; Silva, T; Moreira, R; Silva, MF; Filipe, V; Rocha, LF;

Publicação
INTERNATIONAL JOURNAL OF ADVANCED MANUFACTURING TECHNOLOGY

Abstract
The growing demand for high-quality components in various industries, particularly in the automotive sector, requires advanced and reliable inspection methods to maintain competitive standards and support innovation. Manual quality inspection tasks are often inefficient and prone to errors due to their repetitive nature and subjectivity, which can lead to attention lapses and operator fatigue. The inspection of reflective aluminum parts presents additional challenges, as uncontrolled reflections and glare can obscure defects and reduce the reliability of conventional vision-based methods. Addressing these challenges requires optimized illumination strategies and robust image processing techniques to enhance defect visibility. This work presents the development of an automated optical inspection system for reflective parts, focusing on components made of high-pressure diecast aluminum used in the automotive industry. The reflective nature of these parts introduces challenges for defect detection, requiring optimized illumination and imaging methods. The system applies deep learning algorithms and uses dome light to achieve uniform illumination, enabling the detection of small defects on reflective surfaces. A collaborative robotic manipulator equipped with a gripper handles the parts during inspection, ensuring precise positioning and repeatability, which improves both the efficiency and effectiveness of the inspection process. A flow execution-based software platform integrates all system components, enabling seamless operation. The system was evaluated with Schmidt Light Metal Group using three custom datasets to detect surface porosities and inner wall defects post-machining. For surface porosity detection, YOLOv8-Mosaic, trained with cropped images to reduce background noise, achieved a recall value of 84.71% and was selected for implementation. Additionally, an endoscopic camera was used in a preliminary study to detect defects within the inner walls of holes. The industrial trials produced promising results, demonstrating the feasibility of implementing a vision-based automated inspection system in various industries. The system improves inspection accuracy and efficiency while reducing material waste and operator fatigue.

2025

Deep Learning for Multi-class Diagnosis of Thyroid Disorders Using Selective Features

Autores
Santana, F; Brito, J; Georgieva, P;

Publicação
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
Data-based approach for diagnosis of thyroid disorders is still at its early stage. Most of the research outcomes deal with binary classification of the disorders, i.e. presence or not of some pathology (cancer, hyperthyroidism, hypothyroidism, etc.). In this paper we explore deep learning (DL) models to improve the multi-class diagnosis of thyroid disorders, namely hypothyroid, hyperthyroid and no pathology thyroid. The proposed DL models, including DNN, CNN, LSTM, and a hybrid CNN-LSTM architecture, are inspired by state-of-the-art work and demonstrate superior performance, largely due to careful feature selection and the application of SMOTE for class balancing prior to model training. Our experiments show that the CNN-LSTM model achieved the highest overall accuracy of 99%, with precision, recall, and F1-scores all exceeding 92% across the three classes. The use of SMOTE for class balancing improved most of the model’s performance. These results indicate that the proposed DL models not only effectively distinguish between different thyroid conditions but also hold promise for practical implementation in clinical settings, potentially supporting healthcare professionals in more accurate and efficient diagnosis. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

  • 6
  • 4028