Verificação Formal de Código Fonte de Sistema Embarcado em um Veículo Aéreo Não Tripulado - Fleck, Ana Paula; Silva, Guilherme Prudente da; Becker, Leandro Buss (Anais Estendidos do Simpósio Brasileiro de Engenharia de Sistemas Computacionais (SBESC); 2025: Anais Estendidos do XV Simpósio de Engenharia de Sistemas ComputacionaisDO - 10.5753/sbesc_estendido.2025.15314, 2025)
Este trabalho apresenta a aplicação de verificação formal em sistemas embarcados críticos, com foco na análise estática do código-fonte utilizando a ferramenta ESBMC. Com foco na detecção de vulnerabilidades em tempo de desenvolvimento, foram analisados 27 arquivos do código-fonte, totalizando mais de 10 mil linhas. Para contornar limitações da ferramenta, foram criados arquivos auxiliares contendo funções de entrada específicas, além da utilização de stubs para simular bibliotecas externas como lwIP e FreeRTOS. A análise permitiu identificar falhas relevantes, como acessos fora dos limites de arrays, uso indevido de ponteiros e vazamentos de memória. Os resultados demonstram o potencial da verificação formal para aumentar a robustez e a confiabilidade do sistema, ao mesmo tempo em que evidenciam os desafios relacionados à verificação modular e ao esforço manual necessário para estruturar os testes.