https://repositorio.ufsc.br/handle/123456789/128640 2026-10-18T13:49:10Z https://repositorio.ufsc.br/handle/123456789/277140 Metodologia de geração automática de testes via Model Checking guiada por critério de cobertura MC/DC para validação de sistemas críticos de automação naval Zamberlan, Jhonny Sistemas Críticos de Automação (SCAs) em aplicações de alto risco, como as do setor naval, demandam alta confiabilidade, uma vez que falhas no software de controle podem acarretar consequências catastróficas. Contudo, a validação manual de códigos para Controladores Lógicos Programáveis (CLPs) mostra-se onerosa, sujeita a erros humanos e limitada na cobertura de cenários. Inserida em um ciclo de desenvolvimento assistido por Model Checking (MC), esta dissertação apresenta uma metodologia para a geração automática de casos de teste e oráculos direcionada a SCA navais utilizando teste baseado em MC. O objetivo principal consiste em reutilizar os modelos abstratos da fase de verificação para conceber o plano de testes da etapa de validação. Para tanto, a abordagem utiliza padrões da indústria, como a Matriz de Causa e Efeito (MCE) e o GRAFCET para modelar especificações funcionais e comportamentos sequenciais temporizados. A extração dos casos de teste parte do modelo abstrato traduzido diretamente do Diagrama Lógico Binário (DLB), utilizando a linguagem formal intermediária FIACRE para gerar um Sistema de Transição Temporizado (TTS). Em seguida, a metodologia emprega Diagramas de Decisão Binária (BDD) para extrair os caminhos lógicos que satisfazem o critério de Cobertura Modificada de Condições/Decisões (MC/DC), traduzindo-os sistematicamente em propriedades-armadilha expressas em Lógica Temporal Linear (LTL). Na etapa de verificação, utilizam-se as ferramentas do TINA por meio da técnica de On-the-Fly MC, visando mitigar a explosão de estados e garantir caminhos mais curtos de teste, cujos contraexemplos gerados são reinterpretados como casos de teste. A metodologia foi validada por meio de um estudo de caso do sistema de controle de partida e parada de um motor, implementado em um CLP físico em ambiente de laboratório. O conjunto de testes gerado foi capaz de detectar erros induzidos nas lógicas implementadas no ladder do CLP, demonstrando que a abordagem extrai cenários de teste factíveis que cobrem tanto a ativação quanto a desativação de saídas, estados e transições a partir de cada causa independentemente. A limitação do método, intrínseca a abordagens de caixa-preta, reside na detecção de códigos ocultos não previstos nas funções de ativação originais. Por fim, a estratégia proposta garante uma cobertura satisfatória com baixo custo computacional e de teste, complementando testes manuais e elevando o nível de segurança no ciclo de desenvolvimento de sistemas de automação.; Abstract: Critical Automation Systems (CAS) in high-risk applications, such as in the naval domain, demand high reliability, given that failures in control software can lead to catastrophic consequences. Manual code validation for Programmable Logic Controllers (PLCs) proves to be resource-intensive, error-prone, and limited in scenario coverage. Integrated into a development lifecycle assisted by Model Checking (MC), this dissertation proposes a methodology for the automated generation of test cases and oracles tailored to naval CAS using MC-based testing. The primary objective is to reuse abstract models from the verification phase to design the test plan for the validation phase. To this end, the approach employs industry standards such as the Cause and Effect Matrix (CEM) and GRAFCET to model functional specifications and timed sequential behaviors. Test case extraction from the abstract model translated directly from the Binary Logic Diagram (BLD), utilizing the FIACRE intermediate formal language to generate a Timed Transition System (TTS). Subsequently, the methodology applies Binary Decision Diagrams (BDD) to extract the logical execution paths that satisfy the Modified Condition/Decision Coverage (MC/DC) criterion, systematically translating them into trap properties expressed in Linear Temporal Logic (LTL). In the verification phase, the capabilities of the TINA toolset are leveraged via On-the-Fly MC to mitigate state-space explosion and ensure minimal-length test paths, whose generated counterexamples are reinterpreted as test cases. The methodology was validated through a case study on a motor start and stop control system implemented on a physical PLC in a laboratory environment. The generated test suite successfully detected injected errors in the PLC ladder logic, demonstrating that the approach extracts feasible test scenarios that cover both activation and deactivation of outputs, states, and transitions independently for each cause. A limitation of the method, intrinsic to black-box testing approaches, lies in the detection of hidden code not accounted for in the original activation functions. Finally, the proposed strategy ensures satisfactory coverage with low computational and testing effort, complementing manual testing and enhancing the safety level throughout the automation system development lifecycle. Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2026. 2026-01-01T00:00:00Z https://repositorio.ufsc.br/handle/123456789/277136 Sistema automatizado para ensaios de elevação térmica em inversores de frequência sob diferentes condições de carga Silva, Juliano Ricardo da Este trabalho apresenta o desenvolvimento e a validação de uma bancada automatizada para ensaios de elevação térmica em inversores de frequência, com foco na caracterização dos desempenhos térmico e elétrico do equipamento sob diferentes condições de carga. O método proposto permite determinar os limites operacionais do inversor, mapeando as máximas potências admissíveis sob restrições térmicas de componentes críticos, incluindo elementos passivos, conector, fonte de alimentação chaveada e microcontrolador. Para superar as limitações das abordagens tradicionalmente empregadas nesses ensaios, caracterizadas pela elevada dependência de intervenções manuais, pela alta variabilidade dos resultados e pelos longos tempos de execução, foi concebida uma plataforma integrada de hardware e software capaz de gerenciar autonomamente as condições de ensaio, realizar a aquisição sincronizada das variáveis monitoradas e executar os procedimentos experimentais de forma programável e segura. A implementação contemplou a identificação experimental de modelos dinâmicos, o projeto de uma estrutura de controle em cascata baseada em escalonamento de ganhos para a regulação da potência e em controle restritivo de temperatura, além da avaliação metrológica do sistema de medição. Os resultados evidenciaram elevada estabilidade operacional e repetibilidade dos ensaios, respaldadas por análises metrológicas que indicaram incertezas expandidas de aproximadamente 2,3 ºC para as medições de temperatura e 2,5 W para as medições de potência. Conclui-se que a solução proposta apresenta potencial de aplicação imediata no setor industrial, contribuindo para a padronização de ensaios térmicos em conformidade com diretrizes normativas, para a redução de custos de desenvolvimento, para a aceleração de ciclos de homologação e para o avanço de pesquisas de confiabilidade de sistemas de conversão de potência.; Abstract: This work presents the development and experimental validation of an automated test rig for temperature rise testing of variable frequency drives (VFDs), focusing on the characterization of their thermal and electrical performance under different loading conditions. The proposed method enables the determination of the drive's operational limits by mapping the maximum permissible output power while ensuring compliance with the thermal constraints of critical components, including passive devices, connectors, the switch-mode power supply (SMPS), and the microcontroller. To overcome the limitations of conventional testing approaches, which are characterized by extensive manual intervention, high result variability, and long execution times, an integrated hardware and software platform was developed. The proposed solution is capable of managing test conditions, acquiring and synchronizing measurement data, and executing experimental procedures in a programmable, autonomous, and safe manner. The implementation comprised the experimental identification of dynamic models, the design of a cascade control architecture based on gain scheduling for power regulation and temperature override control, and the metrological assessment of the measurement system. Experimental results demonstrated high operational stability and test repeatability, supported by metrological analyses that yielded expanded uncertainties of approximately 2,3 ºC for temperature measurements and 2,5 W for power measurements. The results demonstrate that the proposed solution is well suited for industrial applications, contributing to the standardization of thermal testing procedures in accordance with regulatory guidelines, reducing development costs, shortening product qualification cycles, and supporting research on the reliability of power electronic conversion systems. Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2026. 2026-01-01T00:00:00Z https://repositorio.ufsc.br/handle/123456789/277127 Um método de calibração para simuladores de redes LoRaWAN em ambientes marítimos Becker, Helmuth Dias A expansão da Internet das Coisas impulsionou o uso de redes LPWAN e de simuladores para o planejamento e a avaliação de sistemas de comunicação sem fio. Entretanto, os modelos de propagação utilizados nesses simuladores, quando em uso com seus parâmetros padronizados, podem apresentar resultados imprecisos quando aplicados a ambientes diferentes daqueles para os quais foram desenvolvidos. Nesse contexto, este trabalho propõe um método de calibração de modelos de perda de percurso para redes LoRaWAN em ambiente marítimo costeiro. Foram coletados dados experimentais de RSSI por meio de um nodo embarcado e de um gateway fixo. Posteriormente, esses dados foram utilizados para calibrar os parâmetros do modelo LoRaLogNormalShadowing no simulador OMNeT++/FLoRa. Os resultados demonstraram que a calibração aproximou os valores simulados dos dados obtidos em campo, reduzindo o erro médio absoluto em comparação com o modelo configurado com parâmetros padrão.; Abstract: The expansion of the Internet of Things has driven the use of LPWAN networks and simulators for the planning and evaluation of wireless communication systems. However, the propagation models used in these simulators, when configured with standardized parameters, may produce inaccurate results when applied to environments different from those for which they were developed. In this context, this work proposes a calibration method for path loss models applied to LoRaWAN networks in a coastal maritime environment. Experimental RSSI data were collected using an onboard node and a fixed gateway. Subsequently, these data were used to calibrate the parameters of the LoRaLogNormalShadowing model in the OMNeT++/FLoRa simulator. Results demonstrate that the calibration brought the simulated values closer to the field measurements, reducing the mean absolute error compared with the model configured with standard parameters. Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2026. 2026-01-01T00:00:00Z https://repositorio.ufsc.br/handle/123456789/276913 Model-based derivative-free optimization with uncertainty handling: applications in petroleum production optimization Hannanu, Muhammad Iffan O tratamento de incertezas em um arcabouço de otimização é um tema importante em diversas áreas da engenharia. Contudo, a incorporação de incertezas pode aumentar drasticamente a demanda por recursos computacionais. Normalmente, nessa situação, recorre-se a métodos baseados em derivadas por sua eficiência; entretanto, isso nem sempre é possível devido à necessidade de modificar de forma intrusiva os códigos-fonte. Nesta tese, apresenta-se um método eficiente de otimização sem derivadas (DFO, do inglês Derivative-Free Optimization) que aborda essas questões. O método DFO proposto é um método de região de confiança sem derivadas baseado em modelos (DFTR, do inglês Derivative-Free Trust Region), que constrói modelos polinomiais para a função objetivo e para as restrições a fim de guiar as iterações até a solução ótima. A vantagem do método é tríplice. Primeiro, o método utiliza pontos previamente avaliados para construir os modelos polinomiais, o que reduz consideravelmente o número necessário de avaliações de função. Segundo, a qualidade do modelo polinomial depende exclusivamente da geometria do conjunto de interpolação, e não da saída, permitindo a escolha ótima de quais pontos avaliar em seguida. Por fim, o uso do método de filtro proporciona uma maneira eficiente de avançar as iterações ao tratar simultaneamente a função objetivo e as restrições. Apresentam-se estudos de caso da aplicação do método de região de confiança sem derivadas, baseado em modelos, em problemas de otimização de plataformas de produção de petróleo. Consideram-se diversos casos com diferentes sistemas de reservatório, funções objetivo e restrições de entrada e de saída. Os estudos de otimização mostram que o DFTR teve desempenho consistentemente bom em todos os problemas. Observa-se que o método proposto é capaz de encontrar soluções satisfatórias com menos avaliações de função em comparação com outros métodos DFO. Além disso, o método DFTR apresenta bom desempenho mesmo partindo de pontos iniciais inviáveis. Em seguida, verifica-se que é possível formular e resolver problemas de otimização mais complexos que tratam incertezas, seja quando a incerteza é representada por um conjunto (ensemble), seja quando é representada por alguma forma de distribuição. Apesar de ser um otimizador local, o método DFTR mostra-se bem adequado a problemas de otimização não linear devido à sua versatilidade e eficiência.; Abstract: Handling of uncertainty in an optimization framework is an important topic in many different fields of engineering. However, the addition of uncertainty may dramatically increase the need for computing resources. Typically in this situation, one would turn into derivative-based solvers for efficiency; however, this is not always possible due to the need to intrusively modify the source codes. In this dissertation, we present an efficient derivative-free optimization (DFO) method which addresses these issues. The proposed DFO method is a model-based derivative-free trust-region (DFTR) method that builds polynomial models for the objective function and constraints to guide the iterations to the optimum solution. The advantage of the method is threefold. First, the method makes use of the previously evaluated points to construct polynomial models, which greatly decrease the required number of function evaluations. Second, the quality of the polynomial model is dependent solely on the geometry of the interpolation set and not the output, thus allowing for optimal choice over which points to evaluate next. Lastly, the use of the filter method provides an efficient way to advance the iterations by handling both the objective and the constraints simultaneously. We present case studies of the use of this method in the context of petroleum subsurface optimization problems. We consider several cases with various petroleum reservoir systems, objective functions, and input and output constraints. Our optimization studies show that DFTR has consistently performed well in all problems. We observe that the proposed method is able to find satisfactory solutions with fewer function evaluations compared to other DFO methods. Further, the DFTR method performs just as well using initial infeasible points. Then, we find that we can formulate and solve more complex optimization problems that handle uncertainty; whether the uncertainty is represented by an ensemble, or when it is represented using some form of distribution. Despite being a local optimizer, the DFTR method proves to be well-suited for nonlinear optimization problems due to its versatility and efficiency. Tese (doutorado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2026. 2026-01-01T00:00:00Z