Mostrar el registro sencillo del documento

Formal verification of the high availability quality attribute for software systems based on microservices architectures

dc.rights.licenseAtribución-NoComercial-CompartirIgual 4.0 Internacional
dc.contributor.advisorVergara Vargas, Jeisson Andrés
dc.contributor.authorDajer Piñerez, Camilo Andres
dc.date.accessioned2023-05-24T16:08:30Z
dc.date.available2023-05-24T16:08:30Z
dc.date.issued2023-04-25
dc.identifier.urihttps://repositorio.unal.edu.co/handle/unal/83851
dc.descriptionilustraciones, graficas
dc.description.abstractThe 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.
dc.description.abstractLas 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)
dc.format.extentxiv, 55 páginas
dc.format.mimetypeapplication/pdf
dc.language.isoeng
dc.publisherUniversidad Nacional de Colombia
dc.rights.urihttp://creativecommons.org/licenses/by-nc-sa/4.0/
dc.subject.ddc000 - Ciencias de la computación, información y obras generales
dc.titleFormal verification of the high availability quality attribute for software systems based on microservices architectures
dc.typeTrabajo de grado - Maestría
dc.type.driverinfo:eu-repo/semantics/masterThesis
dc.type.versioninfo:eu-repo/semantics/acceptedVersion
dc.publisher.programBogotá - Ingeniería - Maestría en Ingeniería - Ingeniería de Sistemas y Computación
dc.contributor.researchgroupColectivo de Investigación en Ingeniería de Software Colswe
dc.description.degreelevelMaestría
dc.description.degreenameMagíster en Ingeniería - Ingeniería de Sistemas y Computación
dc.description.researchareaArquitectura de Software
dc.identifier.instnameUniversidad Nacional de Colombia
dc.identifier.reponameRepositorio Institucional Universidad Nacional de Colombia
dc.identifier.repourlhttps://repositorio.unal.edu.co/
dc.publisher.facultyFacultad de Ingeniería
dc.publisher.placeBogotá, Colombia
dc.publisher.branchUniversidad Nacional de Colombia - Sede Bogotá
dc.relation.referencesAHMAD, Aakash ; BABAR, Muhammad A.: Software architectures for robotic systems: A systematic mapping study. In: Journal of Systems and Software 122 (2016), dec, S. 16–39. http://dx.doi.org/10.1016/j.jss.2016.08.039. – DOI 10.1016/j.jss.2016.08.039. – ISSN 01641212
dc.relation.referencesBABAR, Muhammad A. ; KITCHENHAM, Barbara ; ZHU, Liming ; GORTON, Ian ; JEFFERY, Ross: An empirical study of groupware support for distributed software architecture evaluation process. In: Journal of Systems and Software 79 (2006), jul, Nr. 7, S. 912–925. http://dx.doi. org/10.1016/j.jss.2005.06.043. – DOI 10.1016/j.jss.2005.06.043. – ISSN 01641212
dc.relation.referencesBARBER, K. S. ; GRASER, Thomas ; HOLT, Jim: Providing early feedback in the development cycle through automated application of model checking to software architectures. In: Proceedings - 16th Annual International Conference on Automated Software Engineering, ASE 2001, Institute of Electrical and Electronics Engineers (IEEE), aug 2001. – ISBN 076951426X, S. 341–345
dc.relation.referencesBASS, Len ; CLEMENTS, Paul ; KAZMAN, Rick: Software Architecture in Practice Second Edition Third Edition. 2013. – 576 S. https://www.oreilly.com/library/view/ software-architecture-in/9780132942799/. – ISBN 0321815736
dc.relation.referencesBRITO, Patrick H. ; DE LEMOS, Rogério ; RUBIRA, Cecília M.F. ; MARTINS, Eliane: Architecting fault tolerance with exception handling: Verification and validation. In: Journal of Computer Science and Technology 24 (2009), mar, Nr. 2, S. 212–237. http://dx.doi.org/10.1007/ s11390-009-9219-2. – DOI 10.1007/s11390–009–9219–2. – ISSN 10009000
dc.relation.referencesCAMILLI, Matteo ; GARGANTINI, Angelo ; SCANDURRA, Patrizia ; BELLETTINI, Carlo: Eventbased runtime verification of temporal properties using time basic Petri nets. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bd. 10227 LNCS, Springer Verlag, 2017. – ISBN 9783319572871, S. 115–130
dc.relation.referencesCLEMENTS, Paul ; GARLAN, David ; LITTLE, Reed ; NORD, Robert ; STAFFORD, Judith: Documenting software architectures: Views and beyond. In: Proceedings - International Conference on Software Engineering, 2003. – ISBN 978–1–491–95035–7, 740–741
dc.relation.referencesCZEPA, Christoph ; TRAN, Huy ; ZDUN, Uwe ; TRAN, Thanh ; WEISS, Erhard ; RUHSAM, Christoph: Reduction techniques for efficient behavioral model checking in adaptive case management. In: Proceedings of the ACM Symposium on Applied Computing Bd. Part F1280, Association for Computing Machinery, apr 2017. – ISBN 9781450344869, S. 719–726
dc.relation.referencesDEHKORDI, Zohreh S. ; HAROUNABADI, Ali ; PARSA, Saeed: Evaluation of software architecture using fuzzy color Petri net. In: Management Science Letters 3 (2013), feb, Nr. 2, S. 555–562. http://dx.doi.org/10.5267/J.MSL.2012.12.016. – DOI 10.5267/J.MSL.2012.12.016. – ISSN 19239335
dc.relation.referencesDEMIRLI, Elif ; TEKINERDOGAN, Bedir: Software language engineering of architectural viewpoints. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bd. 6903 LNCS, AMSE Press, mar 2011. – ISBN 9783642237973, S. 336–343
dc.relation.referencesDI FRANCESCO, Paolo ; LAGO, Patricia ; MALAVOLTA, Ivano: Architecting with microservices: A systematic mapping study. In: Journal of Systems and Software 150 (2019), apr, S. 77–97. http://dx.doi.org/10.1016/j.jss.2019.01.001. – DOI 10.1016/j.jss.2019.01.001. – ISSN 01641212
dc.relation.referencesDOBRICA, Liliana ; NIEMELÁ, Eila: A survey on software architecture analysis methods
dc.relation.referencesDRAGONI, Nicola ; GIALLORENZO, Saverio ; LAFUENTE, Alberto L. ; MAZZARA, Manuel ; MONTESI, Fabrizio ; MUSTAFIN, Ruslan ; SAFINA, Larisa: Microservices: Yesterday, today, and tomorrow. Version: nov 2017. http://dx.doi.org/10.1007/978-3-319-67425-4_12. In: Present and Ulterior Software Engineering. Springer International Publishing, nov 2017. – DOI 10.1007/978–3–319–67425–4_12. – ISBN 9783319674254, S. 195–216
dc.relation.referencesFERRARI, Remo ; MADHAVJI, Nazim H.: Software architecting without requirements knowledge and experience: What are the repercussions? In: Journal of Systems and Software 81 (2008), sep, Nr. 9, S. 1470–1490. http://dx.doi.org/10.1016/j.jss.2007.12.764. – DOI 10.1016/j.jss.2007.12.764. – ISSN 01641212
dc.relation.referencesGHEZZI, Carlo ; MANDRIOLI, Dino ; MORASCA, Sandro ; PEZZE, Maura: A unified highlevel Petri net formalism for time-critical systems. In: IEEE Transactions on Software Engineering 17 (1991), feb, Nr. 2, S. 160–172. http://dx.doi.org/10.1109/32.67597. – DOI 10.1109/32.67597. – ISSN 00985589
dc.relation.referencesGIANNAKOPOULOU, Dimitra: Model Checking for Concurrent Software Architecutures. In: Department of Computing (1998), Nr. January. http://www.doc.ic.ac.uk/{~}dg1/tracta/papers/thesis.pdf
dc.relation.referencesHANSEN, Klaus M. ; JONASSON, Kristjan ; NEUKIRCHEN, Helmut: An empirical study of software architectures’ effect on product quality. In: Journal of Systems and Software 84 (2011), jul, Nr. 7, S. 1233–1243. http://dx.doi.org/10.1016/j.jss.2011.02.037. – DOI 10.1016/j.jss.2011.02.037. – ISSN 01641212
dc.relation.referencesHAOUES, Mariem ; SELLAMI, Asma ; BEN-ABDALLAH, Hanêne ; CHEIKHI, Laila: A guideline for software architecture selection based on ISO 25010 quality related characteristics. In: International Journal of System Assurance Engineering and Management 8 (2017), nov, S. 886–909. http://dx.doi.org/10.1007/s13198-016-0546-8. – DOI 10.1007/s13198–016–0546– 8. – ISSN 09764348
dc.relation.referencesHARRISON, Neil B. ; AVGERIOU, Paris: How do architecture patterns and tactics interact? A model and annotation. In: Journal of Systems and Software 83 (2010), oct, Nr. 10, S. 1735–1758. http://dx.doi.org/10.1016/j.jss.2010.04.067. – DOI 10.1016/j.jss.2010.04.067. – ISSN 01641212
dc.relation.referencesHOCKING, Ashlie B. ; KNIGHT, John C. ; AIELLO, M. A. ; SHIRAISHI, Shin’Ichi: Formal Verification in Model Based Development. In: SAE Technical Papers 2015-April (2015), apr, Nr. April. http://dx.doi.org/10.4271/2015-01-0260. – DOI 10.4271/2015–01–0260. – ISSN 01487191
dc.relation.referencesINVERARDI, Paola ; MUCCINI, Henry ; PELLICCIONE, Patrizio: Automated check of architectural models consistency using SPIN. In: Proceedings - 16th Annual International Conference on Automated Software Engineering, ASE 2001, Institute of Electrical and Electronics Engineers (IEEE), aug 2001. – ISBN 076951426X, S. 346–349
dc.relation.referencesJENSEN, Kurt ; KRISTENSEN, Lars M.: Coloured Petri Nets: Modelling and validation of concurrent systems. In: Coloured Petri Nets: Modelling and Validation of Concurrent Systems (2009), 1–384. http://dx.doi.org/10.1007/B95112. – DOI 10.1007/B95112. ISBN 9783642002830
dc.relation.referencesKAZMAN, Rick ; BASS, Len ; KLEIN, Mark ; LATTANZE, Tony ; NORTHROP, Linda: A basis for analyzing software architecture analysis methods
dc.relation.referencesLEWIS, Grace ; LAGO, Patricia ; ECHEVERRÍA, Sebastián ; SIMOENS, Pieter: A tale of three systems: Case studies on the application of architectural tactics for cyber-foraging. In: Future Generation Computer Systems 96 (2019), jul, S. 119–147. http://dx.doi.org/10.1016/j. future.2019.01.052. – DOI 10.1016/j.future.2019.01.052. – ISSN 0167739X
dc.relation.referencesLI, J. J. ; HORGAN, J. R.: Applying formal description techniques to software architectural design. In: Computer Communications 23 (2000), jul, Nr. 12, S. 1169–1178. http://dx.doi. org/10.1016/S0140-3664(99)00244-3. – DOI 10.1016/S0140–3664(99)00244–3. – ISSN 01403664
dc.relation.referencesLI, Shanshan ; ZHANG, He ; JIA, Zijia ; ZHONG, Chenxing ; ZHANG, Cheng ; SHAN, Zhihao ; SHEN, Jinfeng ; BABAR, Muhammad A.: Understanding and addressing quality attributes of microservices architecture: A Systematic literature review
dc.relation.referencesMAGABLEH, Basel ; ALMIANI, Muder: A Self Healing Microservices Architecture: A Case Study in Docker Swarm Cluster. In: Advances in Intelligent Systems and Computing Bd. 926, Springer Verlag, 2020. – ISBN 9783030150310, S. 846–858
dc.relation.referencesMOHSIN, Ahmad ; JANJUA, Naeem K.: A review and future directions of SOA-based software architecture modeling approaches for System of Systems. In: Service Oriented Computing and Applications Bd. 12, Springer London, dec 2018. – ISSN 18632394, S. 183–200
dc.relation.referencesNERI, Davide ; SOLDANI, Jacopo ; ZIMMERMANN, Olaf ; BROGI, Antonio: Design principles, architectural smells and refactorings for microservices: a multivocal review. In: Software- Intensive Cyber-Physical Systems Bd. 35, Springer Science and Business Media LLC, sep 2020. – ISSN 25248529, S. 3–15
dc.relation.referencesNEWMAN, Sam ; .: Building microservices: Designing fine-grained systems (second edition). (2021), S. 1–10. ISBN 9781492034025
dc.relation.referencesNOYLE, Brian (DTS A. ; BOUWMAN, Dave (DTS A.: From Design to Deployment. In: ArcUser (2010), S. 45–47
dc.relation.referencesPARIZEK, Pavel ; PLASIL, Frantisek: Specification and Generation of Environment for Model Checking of Software Components. In: Electronic Notes in Theoretical Computer Science 176 (2007), may, Nr. 2, S. 143–154. http://dx.doi.org/10.1016/j.entcs.2006.02.036. – DOI 10.1016/j.entcs.2006.02.036. – ISSN 15710661
dc.relation.referencesRIM, Kee W. ; MIN, Byoung J. ; SHIN, Sang S.: An Architecture for High Availability Multiuser Systems. In: Computer Communications 20 (1997), may, Nr. 3, S. 197–205. http://dx. doi.org/10.1016/S0140-3664(97)00007-8. – DOI 10.1016/S0140–3664(97)00007–8. – ISSN 01403664
dc.relation.referencesRODANO, Matthew ; GIAMMARCO, Kristin: A formal method for evaluation of a modeled system architecture. In: Procedia Computer Science Bd. 20, Elsevier, 2013. – ISSN 18770509, S. 210–215
dc.relation.referencesROGGENBACH, Markus ; CERONE, Antonio ; SCHLINGLOFF, Bernd-Holger ; SCHNEIDER, Gerardo ; SHAIKH, Siraj A.: Formal methods for software engineering : languages, methods, application domains. ISBN 3030387992
dc.relation.referencesSABRY, Ahmed E.: Decision Model for Software Architectural Tactics Selection Based on Quality Attributes Requirements. In: Procedia Computer Science Bd. 65, Elsevier, 2015. – ISSN 18770509, S. 422–431
dc.relation.referencesSALAMA, Maria ; BAHSOON, Rami: Analysing and modelling runtime architectural stability for self-adaptive software. In: Journal of Systems and Software 133 (2017), nov, S. 95–112. http://dx.doi.org/10.1016/j.jss.2017.07.041. – DOI 10.1016/j.jss.2017.07.041. – ISSN 01641212
dc.relation.referencesSIDDIQUI, Junaid H. ; RAUF, Affan ; GHAFOOR, Maryam A.: Advances in Software Model Checking. Version: jan 2018. http://dx.doi.org/10.1016/bs.adcom.2017. 11.001. In: Advances in Computers Bd. 108. Academic Press Inc., jan 2018. – DOI 10.1016/bs.adcom.2017.11.001. – ISBN 9780128151198, S. 59–89
dc.relation.referencesSIEGEL, Stephen F. ; AVRUNIN, George S.: MODELING MPI PROGRAMS FOR VERIFICATION.
dc.relation.referencesSIPSER, Michael: Introduction to the Theory of Computation. In: ACM SIGACT News 27 (1996), Nr. 1, S. 27–29. http://dx.doi.org/10.1145/230514.571645. – DOI 10.1145/230514.571645. – ISBN 9788131525296
dc.relation.referencesSVAHNBERG, Mikael ; WOHLIN, Claes ; LUNDBERG, Lars ; MATTSSON, Michael: A quality-driven decision-support method for identifying software architecture candidates. In: International Journal of Software Engineering and Knowledge Engineering 13 (2003), oct, Nr. 5, S. 547–573. http://dx.doi.org/10.1142/S0218194003001421. – DOI 10.1142/S0218194003001421. – ISSN 02181940
dc.relation.referencesTALEB-BERROUANE, Mohammed ; KHAN, Faisal ; AMYOTTE, Paul: Bayesian Stochastic Petri Nets (BSPN) - A new modelling tool for dynamic safety and reliability analysis. In: Reliability Engineering and System Safety 193 (2020), jan, S. 106587. http://dx.doi.org/10.1016/j. ress.2019.106587. – DOI 10.1016/j.ress.2019.106587. – ISSN 09518320
dc.relation.referencesTARULLO, Michael: Software architecture theory and practice. In: CrossTalk 24 (2011), Nr. 6, S. 11–15. ISBN 0470167742
dc.relation.referencesTEKINERDOGAN, B. ; OZCAN, O.: Architectural Perspective for Design and Analysis of Scalable Software as a Service Architectures. Version: 2017. http://dx.doi.org/10.1016/ B978-0-12-802855-1.00010-1. In: Managing Trade-offs in Adaptable Software Architectures. Elsevier, 2017. – DOI 10.1016/B978–0–12–802855–1.00010–1. – ISBN 9780128028551, S. 223–245
dc.relation.referencesTEKINERDOGAN, Bedir ; SOZER, Hasan ; AKSIT, Mehmet: Software architecture reliability analysis using failure scenarios. In: Journal of Systems and Software 81 (2008), apr, Nr. 4, S. 558–575. http://dx.doi.org/10.1016/j.jss.2007.10.029. – DOI 10.1016/j.jss.2007.10.029. – ISSN 01641212
dc.relation.referencesTORVEKAR, Nupura ; GAME, Pravin S.: Microservices and Its Applications An Overview. In: International Journal of Computer Sciences and Engineering 7 (2019), apr, Nr. 4, S. 803–809. http://dx.doi.org/10.26438/ijcse/v7i4.803809. – DOI 10.26438/ijcse/v7i4.803809
dc.relation.referencesUL MURAM, Faiz ; TRAN, Huy ; ZDUN, Uwe: Supporting automated containment checking of software behavioural models using model transformations and model checking. In: Science of Computer Programming 174 (2019), apr, S. 38–71. http://dx.doi.org/10.1016/j.scico. 2019.01.005. – DOI 10.1016/j.scico.2019.01.005. – ISSN 01676423
dc.relation.referencesVERGARA-VARGAS, Jeisson ; UMANA-ACOSTA, Henry: A model-driven deployment approach for scaling distributed software architectures on a cloud computing platform. In: Proceedings of the IEEE International Conference on Software Engineering and Service Sciences, ICSESS 2017-November (2018), apr, S. 99–103. http://dx.doi.org/10.1109/ICSESS.2017. 8342873. – DOI 10.1109/ICSESS.2017.8342873. – ISBN 9781538645703
dc.relation.referencesZDUN, Uwe ; NAVARRO, Elena ; LEYMANN, Frank: Ensuring and assessing architecture conformance to microservice decomposition patterns. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bd. 10601 LNCS, Springer Verlag, 2017. – ISBN 9783319690346, S. 411–429
dc.relation.referencesZDUN, Uwe ; STOCKER, Mirko ; ZIMMERMANN, Olaf ; PAUTASSO, Cesare ; LÜBKE, Daniel: Guiding architectural decision making on quality aspects in microservice APIs. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bd. 11236 LNCS, Springer Verlag, 2018. – ISBN 9783030035952, S. 73–89
dc.relation.referencesZHANG, Pengcheng ; MUCCINI, Henry ; LI, Bixin: A classification and comparison of model checking software architecture techniques. In: Journal of Systems and Software 83 (2010), may, Nr. 5, S. 723–744. http://dx.doi.org/10.1016/j.jss.2009.11.709. – DOI 10.1016/j.jss.2009.11.709. – ISSN 01641212
dc.relation.referencesZHOU, Xin ; LI, Shanshan ; CAO, Lingli ; ZHANG, He ; JIA, Zijia ; ZHONG, Chenxing ; SHAN, Zhihao ; BABAR, Muhammad A.: Revisiting the practices and pains of microservice architecture in reality: An industrial inquiry. In: Journal of Systems and Software 195 (2023), 111521. http://dx.doi.org/10.1016/j.jss.2022.111521. – DOI 10.1016/j.jss.2022.111521. – ISSN 01641212
dc.rights.accessrightsinfo:eu-repo/semantics/openAccess
dc.subject.proposalSoftware architecture
dc.subject.proposalQuality attributes
dc.subject.proposalFormal methods
dc.subject.proposalArchitectural tactics
dc.subject.proposalFormal verification
dc.subject.proposalMicroservices architecture
dc.subject.proposalHigh availability
dc.subject.proposalArquitectura de software
dc.subject.proposalAtributos de calidad
dc.subject.proposalMétodos formales
dc.subject.proposalTácticas arquitectónicas
dc.subject.proposalVerificación formal
dc.subject.proposalArquitectura de microservicios
dc.subject.proposalAlta disponibilidad
dc.subject.unescoControl de calidad
dc.subject.unescoQuality control
dc.subject.unescoDiseño arquitectónico
dc.subject.unescoBuilding design
dc.title.translatedVerificación formal del atributo de calidad de alta disponibilidad para sistemas de software basados en arquitecturas de microservicios
dc.type.coarhttp://purl.org/coar/resource_type/c_bdcc
dc.type.coarversionhttp://purl.org/coar/version/c_ab4af688f83e57aa
dc.type.contentText
dc.type.redcolhttp://purl.org/redcol/resource_type/TM
oaire.accessrightshttp://purl.org/coar/access_right/c_abf2
dcterms.audience.professionaldevelopmentEstudiantes
dcterms.audience.professionaldevelopmentInvestigadores
dcterms.audience.professionaldevelopmentMaestros
dcterms.audience.professionaldevelopmentPúblico general


Archivos en el documento

Thumbnail
Nombre:
1020821368.2023.pdf
Tamaño:
11.92Mb
Formato:
PDF
Descripción:
Tesis de Maestría en Ingeniería ...
Descargar

Este documento aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del documento

Atribución-NoComercial-CompartirIgual 4.0 InternacionalEsta obra está bajo licencia internacional Creative Commons Reconocimiento-NoComercial 4.0.Este documento ha sido depositado por parte de el(los) autor(es) bajo la siguiente constancia de depósito