Formal verification of the high availability quality attribute for software systems based on microservices architectures
Cargando...
Archivos
Autores
Dajer Piñerez, Camilo Andres
Director
Tipo de contenido
Document language:
Inglés
Fecha
Título de la revista
ISSN de la revista
Título del volumen
Documentos PDF
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)
Abstract
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.
Palabras clave propuestas
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
Descripción
ilustraciones, graficas