Formal Software Verification for the Internet of Things with Application Validation in 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

Abstract

With the increase in software within embedded systems, formal verification has become more important to ensure product quality by using mathematical models to identify unexpected behaviors during algorithm execution. Among the formal verification techniques, model checking stands out, as it verifies whether a system satisfies specific properties. This is essential for critical IoT systems developed in Java and, more recently, Kotlin. This research aims to apply formal verification to Android applications for IoT, identifying security and memory flaws, with the goal of evaluating the effectiveness of the tools and contributing to the improvement of these systems.

References

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.