FCT: DI - Dissertações de Mestrado
URI permanente para esta coleção:
Navegar
Entradas recentes
- ONLINE INTERACTIVE TOOL FOR LEARNING LOGICAL PROOF SYSTEMSPublication . Carvalho, Diogo da Silva Cagica; Gonçalves, Ricardo; Seco, JoãoFor many areas, including mathematics and computer science, logic is a basic but important topic. In particular, the notions of natural deduction and proof systems for natural deduction are of fundamental interest. Students learning logic benefit from the use of interactive, visual tools where they can solve exercises and receive feedback from their attempts. However, most of these tools are based on installable programs, or static, making it hard to expand them with additional learning material and exercises. The few available online tools and courses focusing on logic also tend to skip the topic of natural deduction. The goal of this thesis is the development of a tool that hosts an interactive, visual proof assistant in which a student can create (or load) a proof and attempt to solve it, occasionally receiving feedback to help the student learn and progress at their own pace. The tool’s design would leverage the work done on previously created tools of this kind and function as a complementary tool for computational logic courses or any course that includes natural deduction. To achieve this, the system must implement basic logic algorithms, feature a logic reasoner for the supported branches of logic, be capable of parsing text into formulas, have mechanisms to provide feedback to users regarding errors and finally some kind of exercise management system, allowing a qualified user to save proofs that can later be loaded by any user, while maintaining the state it was saved as. Finally, it’s intended to leverage its usability for automatic evaluation purposes, by incorporating the system, if possible, with existing online e-learning platforms, such as Moodle.
- Real-Time Interaction with Live Broadcasted EventsPublication . Veiga, André António da; Correia, Nuno; Romão, TeresaIn recent years, Augmented Reality (AR) has surged in popularity due to increasingly accessible system requirements and a growing number of practical applications, coupled with the notable success of recent AR-based video games, which renewed interest in this technology as an entertainment medium. The goal of this dissertation is to create an innovative system that makes use of AR and VR technology in order to allow users to remotely interact with live broadcasted events such as sports car races, participating as virtual players that can be seen among the real-world competitors by spectators watching the broadcast. This project entails two primary challenges: ensuring the seamless integration of virtual players into the source video as they move along the track, and accurately positioning real-world cars within the VR simulation, in which they are represented using 3D models for virtual players to race against. To achieve these objectives, this dissertation covers the design and implementation of a system that enables this level of interactivity. Making use of the versatility of the Unity platform, a racing simulator was developed as a proof-of-concept that receives data from a secondary Python-based application, responsible for processing real-time video streams to determine the positions of cars on the track. This data is used by the simulator to replicate the real-world cars in the virtual environment. In parallel, Unity cameras placed in the virtual track with positions and configurations mirroring their real-world counterparts are used in order to generate an AR view of the gameplay footage merged into the original video. The developed simulator allows players to race against real-world opponents, whose positions are obtained from analysis of the video stream using object detection techniques. It also provides users who wish to spectate the race with an AR-based view of the event from the perspective of one of the real-world cameras, consisting of the original video footage augmented with the gameplay of the virtual participants.
- Creating a Web-Based Solution for a Research Tool on Historical Artists’ MaterialsPublication . Badracim, Neel Dinesh; Knorr, Jorg; Otero, VanessaFounded in 1832, Winsor & Newton emerged as a leading global supplier of artists’ materials, known for its innovations in producing high-quality pigments, oil colours, watercolours, and other essential art supplies. The company’s 19th-century manuscript archive is a unique historical resource that holds fundamental value for studies in art conservation and historical authenticity. The archive includes 85 manuscript books and 47 catalogues, covering detailed records of their materials and production methods, providing an in-depth view of the practices and methods of the time. In 2006, a digital database was introduced to host digitised copies of these original manuscripts, along with complementary information, such as recipe details. Although this solution allows researchers to investigate and reference these materials, it has notable limitations. Due to the commercial sensitivity of the content, access to the database is restricted to specific physical locations, which limits wider accessibility and collaborative use among researchers. Furthermore, the database setup lacks functionality for editing or inserting data, limiting researchers’ ability to contribute additional insights or expand the database with new documents and analyses. To overcome these constraints, this dissertation proposes the creation of a web-based database application designed following the three-tier architecture. It leverages modern open-source technologies, including React, Spring Boot, and PostgreSQL. The web application transforms the previous solution into an accessible online platform, offering additional features for data entry, role-based access, and editing based on user roles, as well as data output capabilities, such as the generation of personalised reports tailored to each user’s needs. This work contributes significantly to the fields of Technical Art History and Con- servation by making a historical archive widely accessible and enabling collaborative contributions to the study of historical art materials, ultimately supporting the archive’s nomination for inclusion in the UNESCO Memory of the World Register.
- End-to-end process managementPublication . Abrantes, Guilherme; Moreira, David; Duarte, SérgioModern business processes often span multiple departments, systems, and organizations, each operating on heterogeneous platforms with their own workflow engines. Although process modeling standards provide a unified representation, executing a single process across multiple engines remains a significant challenge due to differences in execution se- mantics, capabilities, and integration mechanisms. This gap complicates the management of distributed processes and undermines the consistency of end-to-end execution. This thesis develops a solution that enables seamless distributed execution of business processes. A decomposition algorithm was designed to partition a unified process model into engine-specific submodels, each preserving the control flow, logical structure, and data dependencies of the original process. Cross-engine transitions are explicitly represented by handover points, ensuring that execution responsibilities are clearly defined. To coordinate execution across engines, an event-driven communication mechanism was implemented, where structured messages exchanged through a message broker allow engines to resume execution at the correct entry points while maintaining process state and data continuity. The resulting approach demonstrates that distributed execution can be achieved while preserving the integrity of the original process. By combining automated decomposition with event-driven coordination, the solution provides a robust foundation for managing end-to-end business processes across heterogeneous workflow engines.
- Sensor Fusion Server for Maritime SurveillancePublication . Santos, Diogo André Rosado; Silva, João; Duarte, VitorThis dissertation explores the research and development of a Data Fusion Server designed for maritime surveillance, that acquires and merges observational data received from multiple sensors, such as AIS (Automatic Identification System) and radars, in order to continuously track and monitor the different objects in the surveillance area. Ensuring an accurate correlation between observations can be particularly challenging since each sensor takes different features into account and covers distinct areas. It is vital that, when a suspicious target is spotted, the system is able to track it across different sensors, which means that, if the target disappears from the coverage range of a specific sensor, it should still be present in the system, if detected by another one. Additionally, the system must be scalable, allowing for the addition of new sensors without the need to alter the source code as much as possible. This approach ensures the system can keep up with new technologies and changing needs without major changes to the code. The proposed solution provides a system that maintains information about the objects in the surveillance area and operates under varying conditions. It needs to be accurate in the rapid identification of objects and support a continuous tracking of these same objects as they move across different sensor ranges, while also allowing easy insertion of new sensors. The evaluation results confirmed that the proposed system can effectively track mar- itime objects across multiple sensors, maintaining track continuity and accurate state estimation under different conditions. Although challenging scenarios revealed some limitations, the system demonstrates strong potential for deployment in real maritime surveillance environments.
- An AI-Powered Framework for Requirements Engineering: The Case of Use Cases and User StoriesPublication . Simonet, Carolina Vieira; Moreira, Ana; Júnior, JoãoRequirements engineering is a fundamental phase in software development, ensuring that stakeholder needs and constraints are accurately identified, understood, specified, validated and documented. Additionally, discovering requirements is not always straight- forward, as some may not be explicitly stated or immediately evident. This often requires a broader perspective to uncover hidden or emerging needs, an area where AI might provide valuable support. This research explores the integration of Generative AI models to enhance the RE process by automating the generation of RE artifacts. The research question guiding this study is: "How can an AI-powered RE framework optimize the extraction and specification of requirements from a system description?". The outcome of this study is an AI-powered RE method that assists in extracting, contextualizing, and refining requirements from a predefined prompt template. The approach we propose aims generate efficiently a set of foundational requirements artifacts, uncover innovative and non-obvious requirements, and thereby streamline the entire requirements analysis process. The proposed AI-powered RE framework is a structured, multi-stage process designed to guide the GAI through a series of sequential tasks. It is composed of three core components: a Structured Prompt Template that ensures clear and contextually rich inputs; a set of Accompanying Guidelines that provide best practices for human-AI collab- oration; and a Defined Process Model that outlines a systematic, iterative workflow. The framework’s evaluation was conducted using a comparative method, where responses to questionnaires from twenty human RE experts were compared with artifacts generated by the GAI, guided by our framework, using the same system description. The outcomes included a initial set of functional and non-functional requirements, along with structured user stories and use cases, which were found to be consistent with the specifications from the questionnaires. By leveraging GAI, this research seeks to optimize the RE work- flow, ultimately contributing to more efficient software development and higher-quality products.
- SELECTING K IN K-MEANS USING GLOBAL-LOCAL EVIDENCE FROM NORMALIZED WIN FREQUENCIESPublication . Gonçalves, Tomás Manuel Cardoso; Nascimento, SusanaK-means is a widely used partitional clustering algorithm due to its simplicity, low computational cost, and ease of implementation. Its performance, however, is sensitive to the choice of initial centroids and to the specification of the number of clusters 𝐾, challenges that intensify on larger or more complex datasets. This dissertation develops and evaluates a methodology to select K robustly and to compare initialization/model- selection strategies on synthetic and real-world data. We introduce the Frequency-Gap Composite (FGC), a four-stage rule that combines global support—via normalized win frequencies across repeated runs—with local distinctiveness—via a discrete local-gap operator—into a single score, from which the selected 𝐾∗ is obtained. We study the Frequency-Gap Composite (FGC), a four-stage rule that combines global support—via normalized win frequencies across repeated runs - with local distinctiveness - via a discrete local-gap operator - into a single score, from which the selected 𝐾∗ is obtained [79]. We benchmark FGC against two established approaches, Iterative Anomalous Pattern (IAP) and X-means, within a unified experimental pipeline. Across data generators and public benchmarks, FGC generally outperforms or matches the baselines: for synthetic data from DG1 (DC1.2), FGC attains 85% correct 𝐾∗ vs 81% (IAP) and 42% (X-means); on Fränti’s benchmark collection, FGC reaches 88% vs 83%/81%; and on real-world datasets, ≈ 83% vs 78%/9% overall, with IAP leading only in small multiclass families. These results indicate that combining normalized frequency evidence with a local-gap signal is an effective, scalable strategy for selecting K in K-means.
- Unsupervised Document Clustering using Implicit FeaturesPublication . Pio, João Pedro Bordadágua; Silva, JoaquimUnsupervised document classification techniques tend to produce lower quality results compared with their supervised counterparts. This happens because labeled data guides the training of supervised document classification tools in the search for quality features. However, unsupervised document classification tools are able to better escalate and keep up with the increasing quantity of unlabeled textual content available on the internet. As such, developing a solution that improves the quality of unsupervised document clustering results, leading to better pseudo-labels and, as a result, better unsupervised document classifiers, would be of great value. To achieve this, we propose the use of implicit features, a set of features that is commonly left untouched that has the potential of helping clustering algorithms produce better results. To understand how the use of implicit features affects the quality of the clustering results across different document clustering scenarios, we developed a clustering pipeline that uses various commonly used term weighting techniques and different clustering algorithms, leading us to a broader research scope and possibly better conclusions. Also, to make our research more relevant, we compared our unsupervised document clustering using the implicit features approach to the results produced by state-of-the-art neural network models in unsupervised document clustering scenarios. With this research we intend to improve the quality of the results produced by unsu- pervised document clustering tools, leading to unsupervised document classification tools capable of producing results whose quality is possibly equal to the results of supervised document classification tools, so that our tools are able to keep up with demand.
- SAFE AND SOUND LOCK GENERATION WITH DATA-CENTRIC CONCURRENCY CONTROLPublication . Gomes, João Manuel Morais; Ravara, AntónioConcurrent programming is essential for exploiting multi-core architectures but raises challenges such as data races, deadlocks, and starvation. Traditional control-centric synchronization embeds locks directly into program flow, complicating correctness rea- soning in complex systems. The Resource-Centric Concurrency Control (RC3) model offers a data-centric alternative by declaring synchronization requirements at the resource level, simplifying reasoning by centralizing concurrency constraints. RC3 shifts focus from control flow to shared data, aiming for safer and more maintainable concurrency management. A cornerstone property is mutual exclusion, ensuring that only one thread accesses a critical section at a time. To enforce this automatically, RC3 employs the Locking Inference Algorithm, which deduces lock requirements and applies them to shared resources. This thesis verifies that the algorithm satisfies mutual exclusion using formal methods and theorem provers. Although full verification remains difficult due to complex execution flows, significant progress is made in connecting formal reasoning with practical implementation. Contributions include mapping correctness requirements for mutual exclusion, seri- alizability, deadlock freedom, and starvation freedom, integrating formal specifications into the implementation, and extending partial verifications. This provides a rigorous foundation for future verification of reliable concurrent systems.
- Visual Editor for Dynamic Condition Response ChoreographiesPublication . Ferreira, Miguel Loupa; Seco, JoãoDistributed and decentralized systems are increasingly present in critical applications, requiring abstractions that can capture dynamic interactions while ensuring correctness and efficiency. Choreographic programming addresses these challenges by defining global system behavior through participant interactions. Among choreographic approaches, Dynamic Condition Response (DCR) Choreographies stand out for their declarative style and adaptability to evolving environments. This thesis presents the design and development of a Visual Editor for DCR Chore- ographies aimed at simplifying the construction, visualization, and management of dis- tributed systems, particularly swarm systems. Swarm systems consist of decentralized, autonomous entities that coordinate without centralized control, making choreographies essential for defining their global behavior. The editor provides an intuitive drag-and-drop interface, allowing users to visually build complex workflows without coding. The code can be further generated with a single click. The technical approach includes modeling global swarm behaviors, generating code and compiling it, visualizing role-specific pro- jections, and simulating execution. This work contributes to the European Project TaRDIS, aiming to enhance the accessibility and efficiency of swarm systems management through intuitive, reactive visual tools. The evaluation confirmed the editor’s effectiveness. A user study with participants of varying expertise showed low error rates, reasonable task completion times, and high satisfaction. Experts were generally faster, but the performance gap with novices was smaller than expected, indicating accessibility across experience levels. Additional feedback revealed that users found the editor intuitive, visually appealing, and confidence- inspiring. These results demonstrate that the DCR Choreographies Visual Editor not only strengthens the TaRDIS toolchain but also provides a solid foundation for future research and richer tools for decentralized system design.
