Verificação Formal de Código Fonte de Sistema Embarcado em um Veículo Aéreo Não Tripulado
Resumo
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.
Palavras-chave:
Sistemas Embarcados, Sistemas Críticos de Segurança, Verificação Formal, Bounded Model Checking
Referências
J. C. Knight, “Safety critical systems: challenges and directions,” in Proceedings of the 24th International Conference on Software Engineering, ser. ICSE ’02. New York, NY, USA: Association for Computing Machinery, 2002, p. 547–550. [Online]. DOI: 10.1145/581339.581406
A. V. Lara, “Design of an embedded system architecture for a SCS,” Master’s thesis, 2019. [Online]. Available: [link]
F. S. Gonçalves, “Integrated method for designing complex cyber-physical systems,” Ph.D. dissertation, Universidade Federal de Santa Catarina, Florianópolis, Brazil, 2018.
L. Cordeiro and B. Fischer, “Verifying multi-threaded software using smt-based context-bounded model checking,” in Proceedings of the 33rd International Conference on Software Engineering, ser. ICSE ’11. New York, NY, USA: Association for Computing Machinery, 2011, p. 331–340. [Online]. DOI: 10.1145/1985793.1985839
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without bdds,” in Tools and Algorithms for the Construction and Analysis of Systems, W. R. Cleaveland, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 193–207.
C. Baier and J.-P. Katoen, “Principles of model checking,” p. 994, 2008.
J. O. de Souza, “Lsverifier: a bmc approach to identify security vulnerabilities in c open-source software projects,” Master’s thesis, 2023, faculdade de Tecnologia. [Online]. Available: [link]
R. R. Ferreira et al., “Runtime verification of low-level software in a vtol uav,” 2025.
A. V. Lara, “Design of an embedded system architecture for a SCS,” Master’s thesis, 2019. [Online]. Available: [link]
F. S. Gonçalves, “Integrated method for designing complex cyber-physical systems,” Ph.D. dissertation, Universidade Federal de Santa Catarina, Florianópolis, Brazil, 2018.
L. Cordeiro and B. Fischer, “Verifying multi-threaded software using smt-based context-bounded model checking,” in Proceedings of the 33rd International Conference on Software Engineering, ser. ICSE ’11. New York, NY, USA: Association for Computing Machinery, 2011, p. 331–340. [Online]. DOI: 10.1145/1985793.1985839
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without bdds,” in Tools and Algorithms for the Construction and Analysis of Systems, W. R. Cleaveland, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 193–207.
C. Baier and J.-P. Katoen, “Principles of model checking,” p. 994, 2008.
J. O. de Souza, “Lsverifier: a bmc approach to identify security vulnerabilities in c open-source software projects,” Master’s thesis, 2023, faculdade de Tecnologia. [Online]. Available: [link]
R. R. Ferreira et al., “Runtime verification of low-level software in a vtol uav,” 2025.
Publicado
24/11/2025
Como Citar
FLECK, Ana Paula; SILVA, Guilherme Prudente da; BECKER, Leandro Buss.
Verificação Formal de Código Fonte de Sistema Embarcado em um Veículo Aéreo Não Tripulado. In: TRABALHOS EM ANDAMENTO - SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SISTEMAS COMPUTACIONAIS (SBESC), 15. , 2025, Campinas/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2025
.
p. 45-48.
ISSN 2763-9002.
DOI: https://doi.org/10.5753/sbesc_estendido.2025.15314.
