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

ilustraciones, graficas

Autores:: Dajer Piñerez, Camilo Andres

Tipo de recurso:

Fecha de publicación:: 2023

Institución:: Universidad Nacional de Colombia

Repositorio:: Universidad Nacional de Colombia

Idioma:: eng

id	UNACIONAL2_465ff68e7bf16370d2347591cb90ef76
oai_identifier_str	oai:repositorio.unal.edu.co:unal/83851
network_acronym_str	UNACIONAL2
network_name_str	Universidad Nacional de Colombia
repository_id_str
dc.title.eng.fl_str_mv	Formal verification of the high availability quality attribute for software systems based on microservices architectures
dc.title.translated.spa.fl_str_mv	Verificación formal del atributo de calidad de alta disponibilidad para sistemas de software basados en arquitecturas de microservicios
title	Formal verification of the high availability quality attribute for software systems based on microservices architectures
spellingShingle	Formal verification of the high availability quality attribute for software systems based on microservices architectures 000 - Ciencias de la computación, información y obras generales 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 Diseño arquitectónico Quality control Building design
title_short	Formal verification of the high availability quality attribute for software systems based on microservices architectures
title_full	Formal verification of the high availability quality attribute for software systems based on microservices architectures
title_fullStr	Formal verification of the high availability quality attribute for software systems based on microservices architectures
title_full_unstemmed	Formal verification of the high availability quality attribute for software systems based on microservices architectures
title_sort	Formal verification of the high availability quality attribute for software systems based on microservices architectures
dc.creator.fl_str_mv	Dajer Piñerez, Camilo Andres
dc.contributor.advisor.none.fl_str_mv	Vergara Vargas, Jeisson Andrés
dc.contributor.author.none.fl_str_mv	Dajer Piñerez, Camilo Andres
dc.contributor.researchgroup.spa.fl_str_mv	Colectivo de Investigación en Ingeniería de Software Colswe
dc.subject.ddc.spa.fl_str_mv	000 - Ciencias de la computación, información y obras generales
topic	000 - Ciencias de la computación, información y obras generales 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 Diseño arquitectónico Quality control Building design
dc.subject.proposal.eng.fl_str_mv	Software architecture Quality attributes Formal methods Architectural tactics Formal verification Microservices architecture High availability
dc.subject.proposal.spa.fl_str_mv	Arquitectura de software Atributos de calidad Métodos formales Tácticas arquitectónicas Verificación formal Arquitectura de microservicios Alta disponibilidad
dc.subject.unesco.spa.fl_str_mv	Control de calidad Diseño arquitectónico
dc.subject.unesco.eng.fl_str_mv	Quality control Building design
description	ilustraciones, graficas
publishDate	2023
dc.date.accessioned.none.fl_str_mv	2023-05-24T16:08:30Z
dc.date.available.none.fl_str_mv	2023-05-24T16:08:30Z
dc.date.issued.none.fl_str_mv	2023-04-25
dc.type.spa.fl_str_mv	Trabajo de grado - Maestría
dc.type.driver.spa.fl_str_mv	info:eu-repo/semantics/masterThesis
dc.type.version.spa.fl_str_mv	info:eu-repo/semantics/acceptedVersion
dc.type.content.spa.fl_str_mv	Text
dc.type.redcol.spa.fl_str_mv	http://purl.org/redcol/resource_type/TM
status_str	acceptedVersion
dc.identifier.uri.none.fl_str_mv	https://repositorio.unal.edu.co/handle/unal/83851
dc.identifier.instname.spa.fl_str_mv	Universidad Nacional de Colombia
dc.identifier.reponame.spa.fl_str_mv	Repositorio Institucional Universidad Nacional de Colombia
dc.identifier.repourl.spa.fl_str_mv	https://repositorio.unal.edu.co/
url	https://repositorio.unal.edu.co/handle/unal/83851 https://repositorio.unal.edu.co/
identifier_str_mv	Universidad Nacional de Colombia Repositorio Institucional Universidad Nacional de Colombia
dc.language.iso.spa.fl_str_mv	eng
language	eng
dc.relation.references.spa.fl_str_mv	AHMAD, 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 BABAR, 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 BARBER, 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 BASS, 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 BRITO, 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 CAMILLI, 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 CLEMENTS, 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 CZEPA, 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 DEHKORDI, 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 DEMIRLI, 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 DI 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 DOBRICA, Liliana ; NIEMELÁ, Eila: A survey on software architecture analysis methods DRAGONI, 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 FERRARI, 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 GHEZZI, 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 GIANNAKOPOULOU, 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 HANSEN, 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 HAOUES, 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 HARRISON, 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 HOCKING, 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 INVERARDI, 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 JENSEN, 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 KAZMAN, Rick ; BASS, Len ; KLEIN, Mark ; LATTANZE, Tony ; NORTHROP, Linda: A basis for analyzing software architecture analysis methods LEWIS, 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 LI, 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 LI, 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 MAGABLEH, 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 MOHSIN, 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 NERI, 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 NEWMAN, Sam ; .: Building microservices: Designing fine-grained systems (second edition). (2021), S. 1–10. ISBN 9781492034025 NOYLE, Brian (DTS A. ; BOUWMAN, Dave (DTS A.: From Design to Deployment. In: ArcUser (2010), S. 45–47 PARIZEK, 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 RIM, 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 RODANO, 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 ROGGENBACH, Markus ; CERONE, Antonio ; SCHLINGLOFF, Bernd-Holger ; SCHNEIDER, Gerardo ; SHAIKH, Siraj A.: Formal methods for software engineering : languages, methods, application domains. ISBN 3030387992 SABRY, 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 SALAMA, 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 SIDDIQUI, 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 SIEGEL, Stephen F. ; AVRUNIN, George S.: MODELING MPI PROGRAMS FOR VERIFICATION. SIPSER, 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 SVAHNBERG, 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 TALEB-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 TARULLO, Michael: Software architecture theory and practice. In: CrossTalk 24 (2011), Nr. 6, S. 11–15. ISBN 0470167742 TEKINERDOGAN, 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 TEKINERDOGAN, 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 TORVEKAR, 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 UL 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 VERGARA-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 ZDUN, 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 ZDUN, 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 ZHANG, 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 ZHOU, 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.coar.fl_str_mv	http://purl.org/coar/access_right/c_abf2
dc.rights.license.spa.fl_str_mv	Atribución-NoComercial-CompartirIgual 4.0 Internacional
dc.rights.uri.spa.fl_str_mv	http://creativecommons.org/licenses/by-nc-sa/4.0/
dc.rights.accessrights.spa.fl_str_mv	info:eu-repo/semantics/openAccess
rights_invalid_str_mv	Atribución-NoComercial-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-nc-sa/4.0/ http://purl.org/coar/access_right/c_abf2
eu_rights_str_mv	openAccess
dc.format.extent.spa.fl_str_mv	xiv, 55 páginas
dc.format.mimetype.spa.fl_str_mv	application/pdf
dc.publisher.spa.fl_str_mv	Universidad Nacional de Colombia
dc.publisher.program.spa.fl_str_mv	Bogotá - Ingeniería - Maestría en Ingeniería - Ingeniería de Sistemas y Computación
dc.publisher.faculty.spa.fl_str_mv	Facultad de Ingeniería
dc.publisher.place.spa.fl_str_mv	Bogotá, Colombia
dc.publisher.branch.spa.fl_str_mv	Universidad Nacional de Colombia - Sede Bogotá
institution	Universidad Nacional de Colombia
bitstream.url.fl_str_mv	https://repositorio.unal.edu.co/bitstream/unal/83851/1/license.txt https://repositorio.unal.edu.co/bitstream/unal/83851/2/1020821368.2023.pdf https://repositorio.unal.edu.co/bitstream/unal/83851/3/1020821368.2023.pdf.jpg
bitstream.checksum.fl_str_mv	eb34b1cf90b7e1103fc9dfd26be24b4a 4f04f36a1bdc6083d073b649469633f3 815b40afe509a628ee2ff40972195103
bitstream.checksumAlgorithm.fl_str_mv	MD5 MD5 MD5
repository.name.fl_str_mv	Repositorio Institucional Universidad Nacional de Colombia
repository.mail.fl_str_mv	repositorio_nal@unal.edu.co
_version_	1814089899213586432
spelling	Atribución-NoComercial-CompartirIgual 4.0 Internacionalhttp://creativecommons.org/licenses/by-nc-sa/4.0/info:eu-repo/semantics/openAccesshttp://purl.org/coar/access_right/c_abf2Vergara Vargas, Jeisson Andrés8c52f6c65439bbafef22f11a880f2749Dajer Piñerez, Camilo Andres7f3c428a8a178d7ef17bc49ff8fa2195Colectivo de Investigación en Ingeniería de Software Colswe2023-05-24T16:08:30Z2023-05-24T16:08:30Z2023-04-25https://repositorio.unal.edu.co/handle/unal/83851Universidad Nacional de ColombiaRepositorio Institucional Universidad Nacional de Colombiahttps://repositorio.unal.edu.co/ilustraciones, 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)MaestríaMagíster en Ingeniería - Ingeniería de Sistemas y ComputaciónArquitectura de Softwarexiv, 55 páginasapplication/pdfengUniversidad Nacional de ColombiaBogotá - Ingeniería - Maestría en Ingeniería - Ingeniería de Sistemas y ComputaciónFacultad de IngenieríaBogotá, ColombiaUniversidad Nacional de Colombia - Sede Bogotá000 - Ciencias de la computación, información y obras generalesSoftware architectureQuality attributesFormal methodsArchitectural tacticsFormal verificationMicroservices architectureHigh availabilityArquitectura de softwareAtributos de calidadMétodos formalesTácticas arquitectónicasVerificación formalArquitectura de microserviciosAlta disponibilidadControl de calidadDiseño arquitectónicoQuality controlBuilding designFormal verification of the high availability quality attribute for software systems based on microservices architecturesVerificación formal del atributo de calidad de alta disponibilidad para sistemas de software basados en arquitecturas de microserviciosTrabajo de grado - Maestríainfo:eu-repo/semantics/masterThesisinfo:eu-repo/semantics/acceptedVersionTexthttp://purl.org/redcol/resource_type/TMAHMAD, 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 01641212BABAR, 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 01641212BARBER, 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–345BASS, 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 0321815736BRITO, 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 10009000CAMILLI, 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–130CLEMENTS, 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–741CZEPA, 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–726DEHKORDI, 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 19239335DEMIRLI, 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–343DI 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 01641212DOBRICA, Liliana ; NIEMELÁ, Eila: A survey on software architecture analysis methodsDRAGONI, 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–216FERRARI, 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 01641212GHEZZI, 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 00985589GIANNAKOPOULOU, Dimitra: Model Checking for Concurrent Software Architecutures. In: Department of Computing (1998), Nr. January. http://www.doc.ic.ac.uk/{~}dg1/tracta/papers/thesis.pdfHANSEN, 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 01641212HAOUES, 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 09764348HARRISON, 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 01641212HOCKING, 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 01487191INVERARDI, 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–349JENSEN, 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 9783642002830KAZMAN, Rick ; BASS, Len ; KLEIN, Mark ; LATTANZE, Tony ; NORTHROP, Linda: A basis for analyzing software architecture analysis methodsLEWIS, 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 0167739XLI, 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 01403664LI, 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 reviewMAGABLEH, 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–858MOHSIN, 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–200NERI, 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–15NEWMAN, Sam ; .: Building microservices: Designing fine-grained systems (second edition). (2021), S. 1–10. ISBN 9781492034025NOYLE, Brian (DTS A. ; BOUWMAN, Dave (DTS A.: From Design to Deployment. In: ArcUser (2010), S. 45–47PARIZEK, 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 15710661RIM, 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 01403664RODANO, 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–215ROGGENBACH, Markus ; CERONE, Antonio ; SCHLINGLOFF, Bernd-Holger ; SCHNEIDER, Gerardo ; SHAIKH, Siraj A.: Formal methods for software engineering : languages, methods, application domains. ISBN 3030387992SABRY, 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–431SALAMA, 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 01641212SIDDIQUI, 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–89SIEGEL, Stephen F. ; AVRUNIN, George S.: MODELING MPI PROGRAMS FOR VERIFICATION.SIPSER, 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 9788131525296SVAHNBERG, 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 02181940TALEB-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 09518320TARULLO, Michael: Software architecture theory and practice. In: CrossTalk 24 (2011), Nr. 6, S. 11–15. ISBN 0470167742TEKINERDOGAN, 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–245TEKINERDOGAN, 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 01641212TORVEKAR, 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.803809UL 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 01676423VERGARA-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 9781538645703ZDUN, 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–429ZDUN, 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–89ZHANG, 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 01641212ZHOU, 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 01641212EstudiantesInvestigadoresMaestrosPúblico generalLICENSElicense.txtlicense.txttext/plain; charset=utf-85879https://repositorio.unal.edu.co/bitstream/unal/83851/1/license.txteb34b1cf90b7e1103fc9dfd26be24b4aMD51ORIGINAL1020821368.2023.pdf1020821368.2023.pdfTesis de Maestría en Ingeniería de Sistemas y Computaciónapplication/pdf12506620https://repositorio.unal.edu.co/bitstream/unal/83851/2/1020821368.2023.pdf4f04f36a1bdc6083d073b649469633f3MD52THUMBNAIL1020821368.2023.pdf.jpg1020821368.2023.pdf.jpgGenerated Thumbnailimage/jpeg4686https://repositorio.unal.edu.co/bitstream/unal/83851/3/1020821368.2023.pdf.jpg815b40afe509a628ee2ff40972195103MD53unal/83851oai:repositorio.unal.edu.co:unal/838512024-08-06 23:10:37.447Repositorio Institucional Universidad Nacional de Colombiarepositorio_nal@unal.edu.coUEFSVEUgMS4gVMOJUk1JTk9TIERFIExBIExJQ0VOQ0lBIFBBUkEgUFVCTElDQUNJw5NOIERFIE9CUkFTIEVOIEVMIFJFUE9TSVRPUklPIElOU1RJVFVDSU9OQUwgVU5BTC4KCkxvcyBhdXRvcmVzIHkvbyB0aXR1bGFyZXMgZGUgbG9zIGRlcmVjaG9zIHBhdHJpbW9uaWFsZXMgZGUgYXV0b3IsIGNvbmZpZXJlbiBhIGxhIFVuaXZlcnNpZGFkIE5hY2lvbmFsIGRlIENvbG9tYmlhIHVuYSBsaWNlbmNpYSBubyBleGNsdXNpdmEsIGxpbWl0YWRhIHkgZ3JhdHVpdGEgc29icmUgbGEgb2JyYSBxdWUgc2UgaW50ZWdyYSBlbiBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsLCBiYWpvIGxvcyBzaWd1aWVudGVzIHTDqXJtaW5vczoKCgphKQlMb3MgYXV0b3JlcyB5L28gbG9zIHRpdHVsYXJlcyBkZSBsb3MgZGVyZWNob3MgcGF0cmltb25pYWxlcyBkZSBhdXRvciBzb2JyZSBsYSBvYnJhIGNvbmZpZXJlbiBhIGxhIFVuaXZlcnNpZGFkIE5hY2lvbmFsIGRlIENvbG9tYmlhIHVuYSBsaWNlbmNpYSBubyBleGNsdXNpdmEgcGFyYSByZWFsaXphciBsb3Mgc2lndWllbnRlcyBhY3RvcyBzb2JyZSBsYSBvYnJhOiBpKSByZXByb2R1Y2lyIGxhIG9icmEgZGUgbWFuZXJhIGRpZ2l0YWwsIHBlcm1hbmVudGUgbyB0ZW1wb3JhbCwgaW5jbHV5ZW5kbyBlbCBhbG1hY2VuYW1pZW50byBlbGVjdHLDs25pY28sIGFzw60gY29tbyBjb252ZXJ0aXIgZWwgZG9jdW1lbnRvIGVuIGVsIGN1YWwgc2UgZW5jdWVudHJhIGNvbnRlbmlkYSBsYSBvYnJhIGEgY3VhbHF1aWVyIG1lZGlvIG8gZm9ybWF0byBleGlzdGVudGUgYSBsYSBmZWNoYSBkZSBsYSBzdXNjcmlwY2nDs24gZGUgbGEgcHJlc2VudGUgbGljZW5jaWEsIHkgaWkpIGNvbXVuaWNhciBhbCBww7pibGljbyBsYSBvYnJhIHBvciBjdWFscXVpZXIgbWVkaW8gbyBwcm9jZWRpbWllbnRvLCBlbiBtZWRpb3MgYWzDoW1icmljb3MgbyBpbmFsw6FtYnJpY29zLCBpbmNsdXllbmRvIGxhIHB1ZXN0YSBhIGRpc3Bvc2ljacOzbiBlbiBhY2Nlc28gYWJpZXJ0by4gQWRpY2lvbmFsIGEgbG8gYW50ZXJpb3IsIGVsIGF1dG9yIHkvbyB0aXR1bGFyIGF1dG9yaXphIGEgbGEgVW5pdmVyc2lkYWQgTmFjaW9uYWwgZGUgQ29sb21iaWEgcGFyYSBxdWUsIGVuIGxhIHJlcHJvZHVjY2nDs24geSBjb211bmljYWNpw7NuIGFsIHDDumJsaWNvIHF1ZSBsYSBVbml2ZXJzaWRhZCByZWFsaWNlIHNvYnJlIGxhIG9icmEsIGhhZ2EgbWVuY2nDs24gZGUgbWFuZXJhIGV4cHJlc2EgYWwgdGlwbyBkZSBsaWNlbmNpYSBDcmVhdGl2ZSBDb21tb25zIGJham8gbGEgY3VhbCBlbCBhdXRvciB5L28gdGl0dWxhciBkZXNlYSBvZnJlY2VyIHN1IG9icmEgYSBsb3MgdGVyY2Vyb3MgcXVlIGFjY2VkYW4gYSBkaWNoYSBvYnJhIGEgdHJhdsOpcyBkZWwgUmVwb3NpdG9yaW8gSW5zdGl0dWNpb25hbCwgY3VhbmRvIHNlYSBlbCBjYXNvLiBFbCBhdXRvciB5L28gdGl0dWxhciBkZSBsb3MgZGVyZWNob3MgcGF0cmltb25pYWxlcyBkZSBhdXRvciBwb2Ryw6EgZGFyIHBvciB0ZXJtaW5hZGEgbGEgcHJlc2VudGUgbGljZW5jaWEgbWVkaWFudGUgc29saWNpdHVkIGVsZXZhZGEgYSBsYSBEaXJlY2Npw7NuIE5hY2lvbmFsIGRlIEJpYmxpb3RlY2FzIGRlIGxhIFVuaXZlcnNpZGFkIE5hY2lvbmFsIGRlIENvbG9tYmlhLiAKCmIpIAlMb3MgYXV0b3JlcyB5L28gdGl0dWxhcmVzIGRlIGxvcyBkZXJlY2hvcyBwYXRyaW1vbmlhbGVzIGRlIGF1dG9yIHNvYnJlIGxhIG9icmEgY29uZmllcmVuIGxhIGxpY2VuY2lhIHNlw7FhbGFkYSBlbiBlbCBsaXRlcmFsIGEpIGRlbCBwcmVzZW50ZSBkb2N1bWVudG8gcG9yIGVsIHRpZW1wbyBkZSBwcm90ZWNjacOzbiBkZSBsYSBvYnJhIGVuIHRvZG9zIGxvcyBwYcOtc2VzIGRlbCBtdW5kbywgZXN0byBlcywgc2luIGxpbWl0YWNpw7NuIHRlcnJpdG9yaWFsIGFsZ3VuYS4KCmMpCUxvcyBhdXRvcmVzIHkvbyB0aXR1bGFyZXMgZGUgZGVyZWNob3MgcGF0cmltb25pYWxlcyBkZSBhdXRvciBtYW5pZmllc3RhbiBlc3RhciBkZSBhY3VlcmRvIGNvbiBxdWUgbGEgcHJlc2VudGUgbGljZW5jaWEgc2Ugb3RvcmdhIGEgdMOtdHVsbyBncmF0dWl0bywgcG9yIGxvIHRhbnRvLCByZW51bmNpYW4gYSByZWNpYmlyIGN1YWxxdWllciByZXRyaWJ1Y2nDs24gZWNvbsOzbWljYSBvIGVtb2x1bWVudG8gYWxndW5vIHBvciBsYSBwdWJsaWNhY2nDs24sIGRpc3RyaWJ1Y2nDs24sIGNvbXVuaWNhY2nDs24gcMO6YmxpY2EgeSBjdWFscXVpZXIgb3RybyB1c28gcXVlIHNlIGhhZ2EgZW4gbG9zIHTDqXJtaW5vcyBkZSBsYSBwcmVzZW50ZSBsaWNlbmNpYSB5IGRlIGxhIGxpY2VuY2lhIENyZWF0aXZlIENvbW1vbnMgY29uIHF1ZSBzZSBwdWJsaWNhLgoKZCkJUXVpZW5lcyBmaXJtYW4gZWwgcHJlc2VudGUgZG9jdW1lbnRvIGRlY2xhcmFuIHF1ZSBwYXJhIGxhIGNyZWFjacOzbiBkZSBsYSBvYnJhLCBubyBzZSBoYW4gdnVsbmVyYWRvIGxvcyBkZXJlY2hvcyBkZSBwcm9waWVkYWQgaW50ZWxlY3R1YWwsIGluZHVzdHJpYWwsIG1vcmFsZXMgeSBwYXRyaW1vbmlhbGVzIGRlIHRlcmNlcm9zLiBEZSBvdHJhIHBhcnRlLCAgcmVjb25vY2VuIHF1ZSBsYSBVbml2ZXJzaWRhZCBOYWNpb25hbCBkZSBDb2xvbWJpYSBhY3TDumEgY29tbyB1biB0ZXJjZXJvIGRlIGJ1ZW5hIGZlIHkgc2UgZW5jdWVudHJhIGV4ZW50YSBkZSBjdWxwYSBlbiBjYXNvIGRlIHByZXNlbnRhcnNlIGFsZ8O6biB0aXBvIGRlIHJlY2xhbWFjacOzbiBlbiBtYXRlcmlhIGRlIGRlcmVjaG9zIGRlIGF1dG9yIG8gcHJvcGllZGFkIGludGVsZWN0dWFsIGVuIGdlbmVyYWwuIFBvciBsbyB0YW50bywgbG9zIGZpcm1hbnRlcyAgYWNlcHRhbiBxdWUgY29tbyB0aXR1bGFyZXMgw7puaWNvcyBkZSBsb3MgZGVyZWNob3MgcGF0cmltb25pYWxlcyBkZSBhdXRvciwgYXN1bWlyw6FuIHRvZGEgbGEgcmVzcG9uc2FiaWxpZGFkIGNpdmlsLCBhZG1pbmlzdHJhdGl2YSB5L28gcGVuYWwgcXVlIHB1ZWRhIGRlcml2YXJzZSBkZSBsYSBwdWJsaWNhY2nDs24gZGUgbGEgb2JyYS4gIAoKZikJQXV0b3JpemFuIGEgbGEgVW5pdmVyc2lkYWQgTmFjaW9uYWwgZGUgQ29sb21iaWEgaW5jbHVpciBsYSBvYnJhIGVuIGxvcyBhZ3JlZ2Fkb3JlcyBkZSBjb250ZW5pZG9zLCBidXNjYWRvcmVzIGFjYWTDqW1pY29zLCBtZXRhYnVzY2Fkb3Jlcywgw61uZGljZXMgeSBkZW3DoXMgbWVkaW9zIHF1ZSBzZSBlc3RpbWVuIG5lY2VzYXJpb3MgcGFyYSBwcm9tb3ZlciBlbCBhY2Nlc28geSBjb25zdWx0YSBkZSBsYSBtaXNtYS4gCgpnKQlFbiBlbCBjYXNvIGRlIGxhcyB0ZXNpcyBjcmVhZGFzIHBhcmEgb3B0YXIgZG9ibGUgdGl0dWxhY2nDs24sIGxvcyBmaXJtYW50ZXMgc2Vyw6FuIGxvcyByZXNwb25zYWJsZXMgZGUgY29tdW5pY2FyIGEgbGFzIGluc3RpdHVjaW9uZXMgbmFjaW9uYWxlcyBvIGV4dHJhbmplcmFzIGVuIGNvbnZlbmlvLCBsYXMgbGljZW5jaWFzIGRlIGFjY2VzbyBhYmllcnRvIENyZWF0aXZlIENvbW1vbnMgeSBhdXRvcml6YWNpb25lcyBhc2lnbmFkYXMgYSBzdSBvYnJhIHBhcmEgbGEgcHVibGljYWNpw7NuIGVuIGVsIFJlcG9zaXRvcmlvIEluc3RpdHVjaW9uYWwgVU5BTCBkZSBhY3VlcmRvIGNvbiBsYXMgZGlyZWN0cmljZXMgZGUgbGEgUG9sw610aWNhIEdlbmVyYWwgZGUgbGEgQmlibGlvdGVjYSBEaWdpdGFsLgoKCmgpCVNlIGF1dG9yaXphIGEgbGEgVW5pdmVyc2lkYWQgTmFjaW9uYWwgZGUgQ29sb21iaWEgY29tbyByZXNwb25zYWJsZSBkZWwgdHJhdGFtaWVudG8gZGUgZGF0b3MgcGVyc29uYWxlcywgZGUgYWN1ZXJkbyBjb24gbGEgbGV5IDE1ODEgZGUgMjAxMiBlbnRlbmRpZW5kbyBxdWUgc2UgZW5jdWVudHJhbiBiYWpvIG1lZGlkYXMgcXVlIGdhcmFudGl6YW4gbGEgc2VndXJpZGFkLCBjb25maWRlbmNpYWxpZGFkIGUgaW50ZWdyaWRhZCwgeSBzdSB0cmF0YW1pZW50byB0aWVuZSB1bmEgZmluYWxpZGFkIGhpc3TDs3JpY2EsIGVzdGFkw61zdGljYSBvIGNpZW50w61maWNhIHNlZ8O6biBsbyBkaXNwdWVzdG8gZW4gbGEgUG9sw610aWNhIGRlIFRyYXRhbWllbnRvIGRlIERhdG9zIFBlcnNvbmFsZXMuCgoKClBBUlRFIDIuIEFVVE9SSVpBQ0nDk04gUEFSQSBQVUJMSUNBUiBZIFBFUk1JVElSIExBIENPTlNVTFRBIFkgVVNPIERFIE9CUkFTIEVOIEVMIFJFUE9TSVRPUklPIElOU1RJVFVDSU9OQUwgVU5BTC4KClNlIGF1dG9yaXphIGxhIHB1YmxpY2FjacOzbiBlbGVjdHLDs25pY2EsIGNvbnN1bHRhIHkgdXNvIGRlIGxhIG9icmEgcG9yIHBhcnRlIGRlIGxhIFVuaXZlcnNpZGFkIE5hY2lvbmFsIGRlIENvbG9tYmlhIHkgZGUgc3VzIHVzdWFyaW9zIGRlIGxhIHNpZ3VpZW50ZSBtYW5lcmE6CgphLglDb25jZWRvIGxpY2VuY2lhIGVuIGxvcyB0w6lybWlub3Mgc2XDsWFsYWRvcyBlbiBsYSBwYXJ0ZSAxIGRlbCBwcmVzZW50ZSBkb2N1bWVudG8sIGNvbiBlbCBvYmpldGl2byBkZSBxdWUgbGEgb2JyYSBlbnRyZWdhZGEgc2VhIHB1YmxpY2FkYSBlbiBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIFVuaXZlcnNpZGFkIE5hY2lvbmFsIGRlIENvbG9tYmlhIHkgcHVlc3RhIGEgZGlzcG9zaWNpw7NuIGVuIGFjY2VzbyBhYmllcnRvIHBhcmEgc3UgY29uc3VsdGEgcG9yIGxvcyB1c3VhcmlvcyBkZSBsYSBVbml2ZXJzaWRhZCBOYWNpb25hbCBkZSBDb2xvbWJpYSAgYSB0cmF2w6lzIGRlIGludGVybmV0LgoKCgpQQVJURSAzIEFVVE9SSVpBQ0nDk04gREUgVFJBVEFNSUVOVE8gREUgREFUT1MgUEVSU09OQUxFUy4KCkxhIFVuaXZlcnNpZGFkIE5hY2lvbmFsIGRlIENvbG9tYmlhLCBjb21vIHJlc3BvbnNhYmxlIGRlbCBUcmF0YW1pZW50byBkZSBEYXRvcyBQZXJzb25hbGVzLCBpbmZvcm1hIHF1ZSBsb3MgZGF0b3MgZGUgY2Fyw6FjdGVyIHBlcnNvbmFsIHJlY29sZWN0YWRvcyBtZWRpYW50ZSBlc3RlIGZvcm11bGFyaW8sIHNlIGVuY3VlbnRyYW4gYmFqbyBtZWRpZGFzIHF1ZSBnYXJhbnRpemFuIGxhIHNlZ3VyaWRhZCwgY29uZmlkZW5jaWFsaWRhZCBlIGludGVncmlkYWQgeSBzdSB0cmF0YW1pZW50byBzZSByZWFsaXphIGRlIGFjdWVyZG8gYWwgY3VtcGxpbWllbnRvIG5vcm1hdGl2byBkZSBsYSBMZXkgMTU4MSBkZSAyMDEyIHkgZGUgbGEgUG9sw610aWNhIGRlIFRyYXRhbWllbnRvIGRlIERhdG9zIFBlcnNvbmFsZXMgZGUgbGEgVW5pdmVyc2lkYWQgTmFjaW9uYWwgZGUgQ29sb21iaWEuIFB1ZWRlIGVqZXJjZXIgc3VzIGRlcmVjaG9zIGNvbW8gdGl0dWxhciBhIGNvbm9jZXIsIGFjdHVhbGl6YXIsIHJlY3RpZmljYXIgeSByZXZvY2FyIGxhcyBhdXRvcml6YWNpb25lcyBkYWRhcyBhIGxhcyBmaW5hbGlkYWRlcyBhcGxpY2FibGVzIGEgdHJhdsOpcyBkZSBsb3MgY2FuYWxlcyBkaXNwdWVzdG9zIHkgZGlzcG9uaWJsZXMgZW4gd3d3LnVuYWwuZWR1LmNvIG8gZS1tYWlsOiBwcm90ZWNkYXRvc19uYUB1bmFsLmVkdS5jbyIKClRlbmllbmRvIGVuIGN1ZW50YSBsbyBhbnRlcmlvciwgYXV0b3Jpem8gZGUgbWFuZXJhIHZvbHVudGFyaWEsIHByZXZpYSwgZXhwbMOtY2l0YSwgaW5mb3JtYWRhIGUgaW5lcXXDrXZvY2EgYSBsYSBVbml2ZXJzaWRhZCBOYWNpb25hbCBkZSBDb2xvbWJpYSBhIHRyYXRhciBsb3MgZGF0b3MgcGVyc29uYWxlcyBkZSBhY3VlcmRvIGNvbiBsYXMgZmluYWxpZGFkZXMgZXNwZWPDrWZpY2FzIHBhcmEgZWwgZGVzYXJyb2xsbyB5IGVqZXJjaWNpbyBkZSBsYXMgZnVuY2lvbmVzIG1pc2lvbmFsZXMgZGUgZG9jZW5jaWEsIGludmVzdGlnYWNpw7NuIHkgZXh0ZW5zacOzbiwgYXPDrSBjb21vIGxhcyByZWxhY2lvbmVzIGFjYWTDqW1pY2FzLCBsYWJvcmFsZXMsIGNvbnRyYWN0dWFsZXMgeSB0b2RhcyBsYXMgZGVtw6FzIHJlbGFjaW9uYWRhcyBjb24gZWwgb2JqZXRvIHNvY2lhbCBkZSBsYSBVbml2ZXJzaWRhZC4gCgo=

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

Publicaciones similares