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

Vista sencilla de ítem
dc.contributor.advisorVergara Vargas, Jeisson Andrés
dc.contributor.authorDajer Piñerez, Camilo Andres
dc.contributor.researchgroupColectivo de Investigación en Ingeniería de Software Colswespa
dc.date.accessioned2023-05-24T16:08:30Z
dc.date.available2023-05-24T16:08:30Z
dc.date.issued2023-04-25
dc.descriptionilustraciones, graficasspa
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.eng
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)spa
dc.description.degreelevelMaestríaspa
dc.description.degreenameMagíster en Ingeniería - Ingeniería de Sistemas y Computaciónspa
dc.description.researchareaArquitectura de Softwarespa
dc.format.extentxiv, 55 páginasspa
dc.format.mimetypeapplication/pdfspa
dc.identifier.instnameUniversidad Nacional de Colombiaspa
dc.identifier.reponameRepositorio Institucional Universidad Nacional de Colombiaspa
dc.identifier.repourlhttps://repositorio.unal.edu.co/spa
dc.identifier.urihttps://repositorio.unal.edu.co/handle/unal/83851
dc.language.isoengspa
dc.publisherUniversidad Nacional de Colombiaspa
dc.publisher.branchUniversidad Nacional de Colombia - Sede Bogotáspa
dc.publisher.facultyFacultad de Ingenieríaspa
dc.publisher.placeBogotá, Colombiaspa
dc.publisher.programBogotá - Ingeniería - Maestría en Ingeniería - Ingeniería de Sistemas y Computaciónspa
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 01641212spa
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 01641212spa
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–345spa
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 0321815736spa
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 10009000spa
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–130spa
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–741spa
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–726spa
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 19239335spa
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–343spa
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 01641212spa
dc.relation.referencesDOBRICA, Liliana ; NIEMELÁ, Eila: A survey on software architecture analysis methodsspa
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–216spa
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 01641212spa
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 00985589spa
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.pdfspa
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 01641212spa
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 09764348spa
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 01641212spa
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 01487191spa
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–349spa
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 9783642002830spa
dc.relation.referencesKAZMAN, Rick ; BASS, Len ; KLEIN, Mark ; LATTANZE, Tony ; NORTHROP, Linda: A basis for analyzing software architecture analysis methodsspa
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 0167739Xspa
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 01403664spa
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 reviewspa
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–858spa
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–200spa
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–15spa
dc.relation.referencesNEWMAN, Sam ; .: Building microservices: Designing fine-grained systems (second edition). (2021), S. 1–10. ISBN 9781492034025spa
dc.relation.referencesNOYLE, Brian (DTS A. ; BOUWMAN, Dave (DTS A.: From Design to Deployment. In: ArcUser (2010), S. 45–47spa
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 15710661spa
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 01403664spa
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–215spa
dc.relation.referencesROGGENBACH, Markus ; CERONE, Antonio ; SCHLINGLOFF, Bernd-Holger ; SCHNEIDER, Gerardo ; SHAIKH, Siraj A.: Formal methods for software engineering : languages, methods, application domains. ISBN 3030387992spa
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–431spa
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 01641212spa
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–89spa
dc.relation.referencesSIEGEL, Stephen F. ; AVRUNIN, George S.: MODELING MPI PROGRAMS FOR VERIFICATION.spa
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 9788131525296spa
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 02181940spa
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 09518320spa
dc.relation.referencesTARULLO, Michael: Software architecture theory and practice. In: CrossTalk 24 (2011), Nr. 6, S. 11–15. ISBN 0470167742spa
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–245spa
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 01641212spa
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.803809spa
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 01676423spa
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 9781538645703spa
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–429spa
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–89spa
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 01641212spa
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 01641212spa
dc.rights.accessrightsinfo:eu-repo/semantics/openAccessspa
dc.rights.licenseAtribución-NoComercial-CompartirIgual 4.0 Internacionalspa
dc.rights.urihttp://creativecommons.org/licenses/by-nc-sa/4.0/spa
dc.subject.ddc000 - Ciencias de la computación, información y obras generalesspa
dc.subject.proposalSoftware architectureeng
dc.subject.proposalQuality attributeseng
dc.subject.proposalFormal methodseng
dc.subject.proposalArchitectural tacticseng
dc.subject.proposalFormal verificationeng
dc.subject.proposalMicroservices architectureeng
dc.subject.proposalHigh availabilityeng
dc.subject.proposalArquitectura de softwarespa
dc.subject.proposalAtributos de calidadspa
dc.subject.proposalMétodos formalesspa
dc.subject.proposalTácticas arquitectónicasspa
dc.subject.proposalVerificación formalspa
dc.subject.proposalArquitectura de microserviciosspa
dc.subject.proposalAlta disponibilidadspa
dc.subject.unescoControl de calidadspa
dc.subject.unescoQuality controleng
dc.subject.unescoDiseño arquitectónicospa
dc.subject.unescoBuilding designeng
dc.titleFormal verification of the high availability quality attribute for software systems based on microservices architectureseng
dc.title.translatedVerificación formal del atributo de calidad de alta disponibilidad para sistemas de software basados en arquitecturas de microserviciosspa
dc.typeTrabajo de grado - Maestríaspa
dc.type.coarhttp://purl.org/coar/resource_type/c_bdccspa
dc.type.coarversionhttp://purl.org/coar/version/c_ab4af688f83e57aaspa
dc.type.contentTextspa
dc.type.driverinfo:eu-repo/semantics/masterThesisspa
dc.type.redcolhttp://purl.org/redcol/resource_type/TMspa
dc.type.versioninfo:eu-repo/semantics/acceptedVersionspa
dcterms.audience.professionaldevelopmentEstudiantesspa
dcterms.audience.professionaldevelopmentInvestigadoresspa
dcterms.audience.professionaldevelopmentMaestrosspa
dcterms.audience.professionaldevelopmentPúblico generalspa
oaire.accessrightshttp://purl.org/coar/access_right/c_abf2spa

Archivos

Bloque original

Mostrando 1 - 1 de 1
Miniatura
Nombre:
1020821368.2023.pdf
Tamaño:
11.93 MB
Formato:
Adobe Portable Document Format
Descripción:
Tesis de Maestría en Ingeniería de Sistemas y Computación
Descargar

Bloque de licencias

Mostrando 1 - 1 de 1
Miniatura
Nombre:
license.txt
Tamaño:
5.74 KB
Formato:
Item-specific license agreed upon to submission
Descripción:
Descargar

Colecciones

Maestría en Ingeniería - Sistemas y Computación