Generative AI and Formal Verification in Microservice Discovery
DOI:
https://doi.org/10.59471/raia2025225Keywords:
ke Microservices, automatic discovery, large language models, formal verification, Lean TheoremProver, architectural metric, evolutionary prompt engineering, AI-assisted software engineeringAbstract
Designing microservices from textual requirements constitutes a persistent challenge in software engineering due to the ambiguity of natural language and the absence of formal mechanisms to guarantee architectural quality. Within the framework of doctoral research at the Universidad Abierta Interamericana (UAI), we present ArchiGenMS, an evolutionary pipeline that combines generative language models (LLMs) with formal verification in Lean for the automatic discovery of microservices. The proposal integrates evolutionary prompt engineering, structural metrics of cohesion, granularity, and coupling, and automatic validation of architectural constraints. Experiments conducted with public datasets of user stories, such as the g24-unibath case, show that the approach allows generating architectures with high cohesion (LCOMavg = 0.167), controlled granularity (SGMmax = 4), and low coupling (Couplingmax = 1). The results evidence the potential of integrating generative techniques and formal verification to build maintainable and reproducible architectures in greenfield scenarios
Downloads
References
Al-Debagy, O., & Martinek, P. (2020). A metrics framework for evaluating microservices architecture designs. Journal of Web Engineering, 19(3–4), 341-370.
Bajaj, D., Bharti, U., Gupta, I., Gupta, P., & Yadav, A. (2024). GTMicro—Microservice identification approach based on deep NLP transformer model for greenfield developments. International Journal of Information Technology, 16(5), 2751-2761.
Bajaj, D., Goel, A., & Gupta, S. C. (2022). GreenMicro: identifying microservices from use cases in greenfield development. IEEE Access, 10, 67008-67018.
Battaglia, N., García, A. N., & Congiusti, A. (2024). Descubrimiento de Microservicios en Metodologías Ágiles: un mapeo sistemático de la literatura. XXX Congreso Argentino de Ciencias de la Computación (CACIC)(La Plata, 7 al 11 de octubre de 2024).
Clarke, E. M., & Wing, J. M. (1996). Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR), 28(4), 626-643.
Clarke, E., Grumberg, O., & Peled, D. A. (1999). Model checking the mit press. Cambridge, Massachusetts, London, UK, 988.
Dalpiaz, F. (2018, julio). Requirements data sets (user stories). Mendeley Data. https://doi.org/
10.17632/7zbk8zsd8y.1
Esposito, M., Li, X., Moreschini, S., Ahmad, N., Cerny, T., Vaidhyanathan, K., Lenarduzzi, V., & Taibi, D. (2025). Generative AI for Software Architecture. Applications, Trends, Challenges, and Future Directions. arXiv preprint arXiv:2503.13310.
Gross, J. L., Yellen, J., & Anderson, M. (2018). Graph theory and its applications. Chapman; Hall/CRC.
Harman, M., Mansouri, S. A., & Zhang, Y. (2012). Search-based software engineering: Trends, techniques and applications. ACM Computing Surveys (CSUR), 45(1), 1-61.
Hevner, A. R., March, S. T., Park, J., & Ram, S. (2004). Design science in information systems research. MIS quarterly, 75-105.
Kalia, A. K., Xiao, J., Krishna, R., Sinha, S., Vukovic, M., & Banerjee, D. (2021). Mono2micro: a practical and effective tool for decomposing monolithic java applications to microservices. Proceedings of the 29th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering, 1214-1224.
Mitchell, B. S., & Mancoridis, S. (2008). On the evaluation of the bunch search-based software modularization algorithm. Soft Computing, 12(1), 77-93.
Moura, L. d., & Ullrich, S. (2021). The lean 4 theorem prover and programming language. International Conference on Automated Deduction, 625-635.
Narváez, D. (2025). ArchiGenMS: Reproducible Package [Accedido: 22 jul. 2025].
Narváez, D., Battaglia, N., Fernández, A., & Rossi, G. (2025a). Designing microservices using ai: A systematic literature review. Software, 4(1), 6.
Narváez, D., Battaglia, N., Fernández, A., & Rossi, G. (2025b). Descubrimiento automático de microservicios mediante modelos generativos y verificación formal. XXXI Congreso Argentino de Ciencias de la Computación (CACIC) (Viedma, 6 al 10 de octubre de 2025).
Narváez, D., Rossi, G. H., & Battaglia, N. (2024). Aplicación de inteligencia artificial en el diseño de microservicios. XXX Congreso Argentino de Ciencias de la Computación (CACIC) (La Plata, 7 al 11 de octubre de 2024).
Neri, D., Soldani, J., Zimmermann, O., & Brogi, A. (2020). Design principles, architectural smells and refactorings for microservices: a multivocal review. SICS Software-Intensive Cyber-Physical Systems, 35(1), 3-15.
Newman, S. (2021). Building microservices: designing fine-grained systems. .O’Reilly Media, Inc."
Pérez, G., Mostaccio, C., & Antonelli, L. (2025). Análisis comparativo de arquitecturas de NLP para detectar similitudes entre escenarios en español. Workshop on Requirements Engineering (WER).
Stojanovic, T., & Lazarević, S. D. (2023). The application of ChatGPT for identification of microservices. E-business technologies conference proceedings, 3(1), 99-105.
Taibi, D., Lenarduzzi, V., & Pahl, C. (2017). Processes, motivations, and issues for migrating to microservices architectures: An empirical investigation. IEEE Cloud Computing, 4(5), 22-32.
Taibi, D., Lenarduzzi, V., Pahl, C., & Janes, A. (2017). Microservices in agile software development: a workshop-based study into issues, advantages, and disadvantages. Proceedings of the XP2017 Scientific Workshops, 1-5.
Taibi, D., & Systä, K. (2019). A Decomposition and Metric-Based Evaluation Framework for Microservices. https://arxiv.org/abs/1908.08513
Ünlü, H., Kennouche, D. E., Soylu, G. K., & Demirörs, O. (2024). Microservice-based projects in agile world: A structured interview. Information and Software Technology, 165, 107334.
Velepucha, V., & Flores, P. (2023). A survey on microservices architecture: Principles, patterns and migration challenges. IEEE access, 11, 88339-88358.
Vera-Rivera, F. H., Cuadros, E. G. P., Perez, B., Astudillo, H., & Gaona, C. (2023). SEMGROMI—a semantic grouping algorithm to identifying microservices using semantic similarity of user stories. PeerJ Computer Science, 9, e1380.
Zhong, C., Li, S., Huang, H., Liu, X., Chen, Z., Zhang, Y., & Zhang, H. (2024). Domain driven design for microservices: An evidence-based investigation. IEEE Transactions on Software Engineering, 50(6), 1425-1449.
Downloads
Published
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
