Formal verification of the high availability quality attribute for software systems based on microservices architectures
Director
Tipo de contenido
Trabajo de grado - Maestría
Idioma del documento
InglésFecha de publicación
2023-04-25Abstract
The 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.Resumen
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)Palabras clave
Software architecture ; Quality attributes ; Formal methods ; Architectural tactics ; Formal verification ; Microservices architecture ; High availability ; Arquitectura de software ; Atributos de calidad ; Métodos formales ; Tácticas arquitectónicas ; Verificación formal ; Arquitectura de microservicios ; Alta disponibilidad ; Control de calidad ; Quality control ; Diseño arquitectónico ; Building design ;
Descripción Física/Lógica/Digital
ilustraciones, graficas
Colecciones
![Atribución-NoComercial-CompartirIgual 4.0 Internacional](/themes/Mirage2//images/creativecommons/cc-generic.png)