Verificação formal de software embarcado em drones de resgate

Abstract

Este trabalho apresenta a aplicação de técnicas de verificação formal ao software embarcado do projeto ProVANT, um veículo aéreo não tripulado (VANT) desenvolvido em parceria entre a UFSC e a UFMG e voltado para missões de busca e salvamento. Por se tratar de um sistema crítico de segurança, a confiabilidade do código é essencial, uma vez que falhas podem comprometer tanto a missão quanto a integridade do equipamento e das pessoas envolvidas. A metodologia adotada consistiu em aplicar o verificador ESBMC (Efficient SMT-Based Bounded Model Checker) sobre o código embarcado do ProVANT. Esse código, implementado em linguagem C, é executado em placas STM32 Nucleo-F767ZI e contempla funções críticas, incluindo drivers de sensores e atuadores, além de módulos de comunicação e controle. A análise foi conduzida de forma modular, abrangendo 27 arquivos, totalizando 10.674 linhas de código e mais de 220 funções. Para viabilizar a execução dos testes, foram criadas funções auxiliares e utilizados stubs que simulam dependências externas, como lwIP e FreeRTOS. Os resultados indicaram que 13 arquivos puderam ser validados sem apresentar vulnerabilidades, 8 continham falhas relevantes e 6 não puderam ser totalmente testados devido a limitações de tempo e escopo. Entre as principais falhas identificadas estão: acessos fora dos limites de arrays, uso de ponteiros nulos, divisões por zero e vazamentos de memória. Tais problemas poderiam comprometer a estabilidade do sistema, levando a travamentos ou perda de controle do VANT. A partir da análise, ajustes e correções foram realizados, aumentando a robustez e a confiabilidade do software embarcado. Conclui-se que a verificação formal, embora demande esforço significativo de preparação e adaptação do código, mostrou-se uma ferramenta eficaz para detectar vulnerabilidades críticas ainda em tempo de desenvolvimento. Como próximas etapas, prevê-se ampliar a cobertura para os módulos restantes, integrar a verificação entre diferentes partes do sistema e avançar na automação do processo, de modo a reduzir o esforço manual envolvido. Essas ações têm como objetivo tornar o processo mais escalável e aplicável também a outros projetos, consolidando a verificação formal como um recurso estratégico na garantia de segurança de sistemas embarcados críticos.