Atribución-NoComercial-CompartirIgual 4.0 InternacionalVergara Vargas, Jeisson AndrésDajer Piñerez, Camilo Andres2023-05-242023-05-242023-04-25https://repositorio.unal.edu.co/handle/unal/83851ilustraciones, graficasThe decisions made by software architects can have significant repercussions if they are made incorrectly. Therefore, it is crucial to base such decisions on concrete evidence rather than solely relying on heuristic experiences to determine if the architectural design decisions were correct. This approach can help avoid incurring refactoring or reengineering costs in the future. This work proposes a general model for the formal verification of software architectures and presents a case study of an architecture based on microservices for ensuring high availability. Through this thesis, the different steps of the model will be presented, and it will be demonstrated how they should be applied to carry out a formal verification. This verification can guide software architects in making decisions based on formal evidence using automatic verification tools.Las decisiones tomadas por los arquitectos de software pueden tener graves repercusiones si se toman de manera incorrecta. Por lo tanto, es fundamental basar dichas decisiones en evidencias concretas en lugar de depender únicamente de experiencias heurísticas para determinar si las decisiones de diseño arquitectónico fueron correctas. Este enfoque puede ayudar a evitar costos de refactorización o reingeniería en el futuro. Este trabajo propone un modelo general de verificación formal para arquitecturas de software y presenta un caso de estudio de una arquitectura basada en microservicios para asegurar el atributo de calidad de disponibilidad. A lo largo de esta tesis se expondrán los diferentes pasos necesarios para llevar a cabo una verificación formal y se explicará cómo deben aplicarse para guiar a los arquitectos de software en la toma de decisiones basadas en evidencias formales, utilizando herramientas de verificación automáticas. (Texto tomado de la fuente)xiv, 55 páginasapplication/pdfenghttp://creativecommons.org/licenses/by-nc-sa/4.0/000 - Ciencias de la computación, información y obras generalesTrabajo de grado - MaestríaUniversidad Nacional de ColombiaRepositorio Institucional Universidad Nacional de Colombiahttps://repositorio.unal.edu.co/info:eu-repo/semantics/openAccessSoftware architectureQuality attributesFormal methodsArchitectural tacticsFormal verificationMicroservices architectureHigh availabilityArquitectura de softwareAtributos de calidadMétodos formalesTácticas arquitectónicasVerificación formalArquitectura de microserviciosAlta disponibilidadControl de calidadQuality controlDiseño arquitectónicoBuilding design