Verificação Formal de Software para Internet das Coisas com Validação de Aplicações em Kotlin/Java

• Evelim B. Rocha UFAM
• Vandermi J. da Silva UFAM
• Andrey A. de O. Rodrigues UFAM

DOI: https://doi.org/10.5753/connect.2025.12111

Resumo

Com o aumento de softwares em sistemas embarcados, a verificação formal ganha importância para garantir a qualidade dos produtos, utilizando modelos matemáticos para identificar comportamentos imprevistos durante a execução de algoritmos. Dentre as técnicas de verificação formal, destaca-se o model checking, que verifica se um sistema atende a propriedades específicas, sendo essencial para sistemas críticos IoT desenvolvidas em Java e, mais recentemente, Kotlin. Esta pesquisa visa aplicar verificações formais em aplicações Android para IoT, identificando falhas de segurança e memória, com o objetivo de avaliar a eficácia das ferramentas e contribuir para a melhoria desses sistemas.

Referências

Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., and Zhu, Y. (2009). Bounded model checking. Handbook of satisfiability, 185(99):457–481.

Clarke, E. M. (1997). Model checking. In Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17, pages 54–56. Springer.

Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., and Trtik, M. (2018). Jbmc: A bounded model checking tool for verifying java bytecode. In International Conference on Computer Aided Verification, pages 183–190. Springer.

Isloor, S. S. and Marsland, T. A. (1980). The deadlock problem: An overview. Computer, 13(9):58–78.

Kahsai, T., Rümmer, P., and Schäf, M. (2019). Jayhorn: A java model checker: (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III 25, pages 214–218. Springer.

Menezes, R., Moura, D., Cavalcante, H., de Freitas, R., and Cordeiro, L. C. (2022). Esbmc-jimple: verifying kotlin programs via jimple intermediate representation. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 777–780.

Mihocka, D. and Troeger, J. (2010). A proposal for hardware-assisted arithmetic overflow detection for array and bitfield operations. In WISH—Workshop on Infrastructures for Software/Hardware Co-Design. Citeseer.

Monteiro, F. R., Gadelha, M. R., and Cordeiro, L. C. (2022). Model checking c++ programs. Software Testing, Verification and Reliability, 32(1):e1793.

Moraes, A. d. and Hayashi, V. (2021). Segurança em IoT: Entendendo os Riscos e Ameaças em IoT. Alta Books. Editora Alta Books.

Pozniansky, E. and Schuster, A. (2003). Efficient on-the-fly data race detection in multithreaded c++ programs. In Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 179–190.

Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L., and Fischer, B. (2013). Smt-based bounded model checking of c++ programs. In 2013 20th IEEE International Conference and Workshops on Engineering of Computer Based Systems (ECBS), pages 147–156. IEEE.

Rowland, C., Goodman, E., Charlier, M., Light, A., and Lui, A. (2015). Designing connected products: UX for the consumer Internet of Things. ”O’Reilly Media, Inc.”.

SILVA, V. J., CORDEIRO, L. C., and JÚNIOR, V. F. D. L. (2013). Verificação de aplicações ami usando java pathfinder.

Weninger, M., Gander, E., and Mössenböck, H. (2019). Analyzing data structure growth over time to facilitate memory leak detection. In Proceedings of the 2019 ACM/SPEC International Conference on Performance Engineering, pages 273–284.