ISEP - DM - Engenharia de Sistemas Computacionais Críticos
URI permanente para esta coleção:
Navegar
Percorrer ISEP - DM - Engenharia de Sistemas Computacionais Críticos por Domínios Científicos e Tecnológicos (FOS) "Engenharia e Tecnologia"
A mostrar 1 - 10 de 19
Resultados por página
Opções de ordenação
- Abordagem à especificação e verificação de requisitos: Caso de estudo em Updates via Over the AirPublication . CARVALHO, ANAISA CRISTINA PEREIRA; Pereira, David Miguel Ramalho; Pinho, Luís Miguel Rosário da SilvaModern vehicles rely on increasingly complex embedded software to deliver advanced features in performance, safety, and connectivity. In automotive software development, a precise requirement specification is essential to manage complexity and ensure reliability throughout the life cycle. Although natural language has been standard for documenting requirements, it often introduces ambiguity and misinterpretation. This thesis focuses on investigating the advantages of adopting formal requirements engineering over natural language approaches within the automotive field, using the Formal Requirements Elicitation Tool (FRET) tool and taking as use case a representative set of requirements of an Over-the-Air (OTA) updates project derived from the automotive industry. This analysis highlights how FRET improves clarity when eliciting, managing, analysis, and verifying requirements, thus serving as a strong asset for reducing errors in later development phases, which is specially important in critical projects. This work also provides evidence of the tangible benefits of formal techniques for the specification, analysis, and verification of vehicle software requirements, but also highlights that tools such as FRET still require formal logic training and, given the niche nature of the tool, that users maintain regular interaction with the developers in order to be aware of features that are fundamental for better usage of the tool, however that still remain undocumented in the literature.
- Application of model checking in the formal verification of requirements for a speed control system in railwayPublication . COELHO, CRISTIANO MANUEL GARCÊS; Pinho, Luís Miguel Rosário da SilvaRailway speed control systems are essential for the safety and efficiency of railway transportation systems, as they ensure compliance with regulations and prevent accidents. As the demand for rail transport grows, rigorous verification of these systems is becomes increasingly critical. In such projects, errors are sometimes only detected during the testing phase, leading to costs that could have been avoided if these errors were identified in the early stages of the project. This thesis focuses on the topic of the formal verification of speed control system, specifically using model checking, to ensure that these systems meet safety requirements as well as performance standards. As the basis for the work presented in this thesis, we will adopt the EBICAB 700 architecture, and for which a small, yet representative, set of safety, operational, or regulatory requirements will be rigorously specified using well-known temporal logic languages, and verified against the system models using the model checking tools NuSMV and UPPAAL. This thesis work aims at contributing to the effort of demonstrating the feasibility and benefits of applying formal verification to railway systems, not only in terms of safety assurance but also as a strategy for reducing late-stage development risks and increased costs. It highlights the value of incorporating formal methods into the requirements and design phases of critical system engineering.
- Authority Handover Procedure and Safety Decision Strategy in Unmanned Aerial VehiclesPublication . Ferreira, Gleizielly Alves; Tovar, Eduardo Manuel MedicisOver recent years, Unmanned Aerial Vehicles (UAVs) applications have become popular in different areas, such as aerial image acquisition, agriculture, inspection and maintenance, mapping, and delivery services. Some of these services require the ability to fly UAVs Beyond Visual Line of Sight (BVLOS) to cover greater distances. Data provided by onboard instruments control the BVLOS operation. The flight controller is responsible for directing the drone flight by controlling the motor’s speed and gathering sensor data. The relevant information about the aircraft, such as position, altitude, speed, and direction of flight, are transmitted via a radio link that informs an operator or a Ground Control Station (GCS). In some drone architectures, there is also an extra computer known as a companion computer or mission computer. They are responsible for providing more intelligence to the flight controller by changing flight parameters. The tasks running on a companion computer can add the capacity to make intelligent decisions during autonomous flight or emergencies, for instance, when the drone loses the radio link with GCS. In addition, for complex drone operations in larger coverage areas, it is necessary to transfer wireless communication links from one access point to another without experiencing connectivity loss. This procedure is known as Handover, and there is much research in this area. Therefore, studies in this field are still needed to find better solutions to avoid failures and increase public and regulatory acceptance of BVLOS operations with UAVs. In this context, the thesis intends to address solutions to the security authorization handover procedure and addresses security strategies in case of a loss of connection.
- Co-simulation of vehicle distributed perception for road safety applicationsPublication . COSTA, TIAGO FILIPE LONGO; Severino, Ricardo Augusto Rodrigues da SilvaThe fast evolution of autonomous vehicles has introduced many new challenges, especially in perception, communication reliability, and energy efficiency. Traditional autonomous vehicles rely on onboard sensors, which are traditionally limited by range, computational cost, and occlusions. The goal of this thesis is to explore the integration of distributed perception systems to enhance situational awareness and improve autonomous vehicles decision-making. This work introduces an extension of the previously established co-simulation framework of Oliveira 2023 and Ribeiro 2024. The solution expands the capabilities of autonomous vehicles to sense beyond the onboard sensors while facilitating safe and efficient merging under different traffic conditions using roadside cameras and a roadside unit. The framework incorporates YOLO-based object detection with trilateration to combine data from a multicamera setup for improved localization accuracy and detection robustness across various traffic conditions. The experimental results show that compared to single-camera configurations, multi-camera fusion significantly increased recall and improved localization levels in conditions with different traffic and perception conditions. The roadside unit can also identify gaps for a safe and efficient merging and provide a target speed to the ego-vehicle via a simulated V2X communication. Overall, the proposed framework demonstrates the feasibility of infrastructure-assisted cooperative perception, providing a realistic and extensible testbed for future research in distributed perception, sensor fusion, and V2X communication for road safety applications.
- Controlo e Monitorização do Ar InternoPublication . Silva, Jorge Manuel e; Barros, António Manuel de SousaMaintaining reliable and secure operation of an organization's servers is an arduous task that requires continuous monitoring and control of several factors. Controlling the operating environment of a server (e.g. temperature and humidity) is critical, as deviations from the equipment's nominal operating conditions can compromise the processes that depend on them, with a consequent negative impact on the organization. Idealizing and prototyping a final product is a laborious process, as its conditions vary from organization to organization. For each case, it is essential to think, idealize, plan and, finally, execute. This project's main objective is to monitor and control the environmental conditions present in a rack through sensors and actuators. The sampled data is integrated into an application that determines the actions that allow maintaining the best operating conditions and preventing/detecting the occurrence of accidents in order to minimize the possibility of loss of resources and critical data.
- Deployment of ML Mechanisms for Cybersecurity in Resource-Constrained Embedded SystemsPublication . Vicente, Pedro Miguel Casal; Santos, Pedro Miguel Salgueiro dosThe increase of low security devices in the Internet is being exploited by hackers to compro mise data or use to use them as external agents to perform further attacks. As so, it is of crucial importance that networks posses a system that correctly assess the nature of incom ing and outgoing packets to protect the local network and the overall Internet connected systems. To achieve this, Machine Learning is being broadly used due to his early success. Nevertheless, these mechanisms are better inserted at the entry point of local networks, an embedded system which has limited resources to train machine learning models and/or to perform inference tasks. Since Cybersecurity is a real-time problem, the embedded systems should perform these activities in a very restricted time interval. The time required to clas sify the packets depends on the overall system load, machine learning models complexity and desired accuracy. This thesis aims to assess the current support for ML in embedded systems, either through the interoperability of models or through their development in low level languages, and the relationship between the time required by different embedded sys tems, the different tools and models. This thesis explored one transpilation tool, m2cgen, two interoperability formats, PMML and Open Neural Network Exchange (ONNX) and one real time environment, ONNXRuntime, to deploy an already trained model in a device with limited resources. Results demonstrate that ONNXRuntime was the only machine learn ing tool with a perfect match regarding samples prediction’s classification from the original models. An analysis on the time required to execute this task revealed that ONNXRun time is faster than Scikit-Learn with the Isolation Forest (ISO), One Class Support Vector Machine (OCSVM) and Stochastic Gradient Descent One Class Support Vector Machine (SGDOCSVM) models and slower with the Local Outlier Factor (LOF) model.
- Development of an Intelligent and Efficient System for Monitoring and Optimising Sailboat PerformancePublication . TEIXEIRA, HENRIQUE MANUEL DE ALMEIDA E SILVA DOS SANTOS; Ferreira, Luis Miguel Moreira LinoThis thesis introduces an AI-powered tool that improves the analysis of sailing performance by automatically detecting thin, high-visibility stripes on sails. It uses computer vision and deep learning to extract key aerodynamic parameters, such as camber, draft, and twist. These parameters are essential for understanding sail shape and enhancing performance. The motivation lies in reducing reliance on traditional manual estimation methods while ensuring efficient onboard processing with lightweight devices like a GoPro camera connected to a tablet. The research starts with a review of current computer vision and AIbased image processing techniques. It also includes a sailing-specific look at the structural and aerodynamic features of sails. Several AI methods - Feature Extraction, Line Detection, Object Detection and Recognition, and Image Segmentation - are compared in this context. The analysis finds that semantic segmentation is the best technique for the goals of this thesis. A further comparison of semantic segmentation models - SegFormer, DeepLab, SAM, and Fast-SCNN - evaluated their accuracy, efficiency, and use for real-time deployment. This review shows that SegFormer is the most effective method for detecting lines in highresolution images of a sailboat's sail. The evaluation carried out in this thesis compares a traditional algorithm, developed in a previous thesis and reused here as a baseline, with an AI-based approach that uses the SegFormer model. This implementation relies on the SegFormer mit-b1 backbone, chosen for its balance between accuracy and efficiency. Mitb2 and mit-b3 were also tested for segmentation quality and processing time comparisons. The evaluation used a dataset of 23 videos and measured how well both methods could reliably detect lines for extracting aerodynamic parameters. The results show a clear tradeoff. The traditional method consistently produced faster processing times because it relies on lightweight operations optimised for CPU use. In contrast, the SegFormer model offered more accurate and reliable line segmentation but required more computational power. Among the tested backbones, SegFormer mit-b1 was the best choice, as mit-b2 and mit-b3 resulted in significantly longer processing times without substantial improvements in segmentation accuracy. In conclusion, the traditional algorithm is still beneficial when speed and limited resources are critical. However, the AI-based approach, especially with SegFormer mit-b1, stands out as a reliable and precise option when more computational resources are available. This work illustrates the potential to integrate AI-driven computer vision into sailing performance analysis, aiding in the accurate and automated extraction of aerodynamic parameters to enhance decision-making and performance improvement in sailing.
- Explorar comunicação V2X para reforçar a segurança em colisões de veículos autónomosPublication . MOREIRA, RODRIGO OLIVEIRA SANTOS; Severino, Ricardo Augusto Rodrigues da SilvaEnsuring safety in autonomous vehicles in complex traffic scenarios is arguably still one of the most important intelligent transport system challenges. Conventional perception systems that depend on sensors such as cameras, LiDAR, and radar are prone to line-of-sight-relevant constraints, adverse weather conditions, and occlusions that can impede threat detection in scenarios of blind turns or obstructed intersections. Vehicle-to-Everything (V2X) communication is also hailed as the hopeful add-on to enhance situational awareness outside vehicle sensor range, where cars may exchange position, velocity, brake, and intent data in real-time. This thesis investigates the application of V2X communication to enhance crash safety by developing a simulation infrastructure that integrates Unreal Engine 5 for photo-realistic scenario simulation and the eCAL middleware for lightweight, low-latency message passing. The infrastructure was developed to simulate cooperative perception for low-visibility scenarios, aiming to establish whether early communication introduces longer reaction times and allows for earlier pre-crash safety system activation, i.e., airbags. Even though the integration of a network simulator (OMNeT++) is incomplete as the compilers and toolchains are not compatible, the project has a simulated working environment using Unreal Engine 5 and ensures eCAL’s role in passing structured data using Protobuf. Experimental results indicate seamless communication between virtual vehicles with near-zero latency, which depicts the potential as well as the limitations of shared-memory communication without real-world network simulation. This parer results provide a clearer vision of the role played by V2X in complementing legacy perception systems on autonomous vehicles. They also herald the need for toolchain synchronizations and simulator compatibilities in follow-on efforts. While the framework is incomplete, it is structured to naturally generalize to more complicated scenarios, heterogeneous sensor fusion, and full real-time synchronization with network simulators. Lastly, this research confirms the standing of V2X as one of the foremost enablers of cooperative safety applications in the quest for safer autonomous driving.
- Formal analysis of an authority transfer protocol for UAVsPublication . Rodrigues, Ricardo Alexandre Almeida; Pereira, David Miguel RamalhoThe use of Unmanned Aerial Vehicles (UAVs) in a variety of applications has resulted in a growing demand for Beyond Visual Line of Sight (BVLOS) operations to cover long distances. This thesis focuses on an initial analysis of a UAV communication protocol designed for transferring control authority between ground controls within a common range, addressing challenges and evaluating its efficacy across different operational phases. The research encompasses start-up, mission execution, and handover phases, assessing the protocol’s interactions with ground-based systems for reliability, efficiency, and adaptability. A comprehensive overview of model checking is provided, emphasizing transition systems, formalisms, and tools for system correctness verification. The research employs model checking to formally specify and model the UAV communication protocol, establishing evaluation criteria through the use of LTL and CTL properties. The derived requirements serve as a foundational framework for future iterations, ensuring the protocol’s robustness and addressing security strategies in the event of connection loss. The holistic approach contributes to a comprehensive understanding of the protocol’s functionality, aiming to enhance the security authorization handover procedure and promote public and regulatory acceptance of BVLOS operations with UAVs.
- Improvement and Modernization of Corporate Virtualization Infrastructure: An Approach to Mitigate Risks and Enhance EfficiencyPublication . DIAS, JOÃO TIAGO TEIXEIRA DA ROCHA; Maio, Paulo Alexandre Fangueiro OliveiraThis dissertation investigates the modernization of a corporate virtualization estate whose Nuxis-based platform has reached end-of-life. A risk-driven evaluation framework is defined to compare technical, operational, and economic options, supported by a state-of-the-art synthesis of hypervisors and management stacks. Requirements and acceptance criteria are made explicit to guide decision-making across availability, disaster recovery, security/governance, observability, automation, and cost (TCO/ROI). A controlled proof-of-concept (PoC) validates key platform behaviors on a single representative virtual machine, exercising live migration, backup/restore, remote backup replication, centralized log forwarding, and API/RBAC enforcement. The results indicate feasibility under laboratory constraints and outline a migration path consistent with a hybrid strategy. The work does not include formal performance or scalability benchmarks; external validity is therefore limited and discussed as a threat. Future work proposes a staged pilot (8–12 heterogeneous VMs) with capacity exercises and production-grade economic assessment to generalize the findings.