Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool

The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a formula to inductive properties of the underlying equational theory by means o...

Full description

Autores:
Rocha, Camilo
Meseguer, José
Tipo de recurso:
Part of book
Fecha de publicación:
2014
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1882
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1882
Palabra clave:
Comprobación del modelo
Regla de inferencia
Propiedad de seguridad
Flujo de entrada
Obligación de prueba
Model Check
Inference Rule
Safety Property
Input Stream
Proof Obligation
Rights
closedAccess
License
© Springer-Verlag Berlin Heidelberg 2014
id ESCUELAIG2_9016b397eb65ee22b31e88c4be827806
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/1882
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.eng.fl_str_mv Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
title Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
spellingShingle Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
Comprobación del modelo
Regla de inferencia
Propiedad de seguridad
Flujo de entrada
Obligación de prueba
Model Check
Inference Rule
Safety Property
Input Stream
Proof Obligation
title_short Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
title_full Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
title_fullStr Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
title_full_unstemmed Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
title_sort Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
dc.creator.fl_str_mv Rocha, Camilo
Meseguer, José
dc.contributor.author.none.fl_str_mv Rocha, Camilo
Meseguer, José
dc.contributor.researchgroup.spa.fl_str_mv Informática
dc.subject.armarc.SPA.fl_str_mv Comprobación del modelo
Regla de inferencia
Propiedad de seguridad
Flujo de entrada
Obligación de prueba
topic Comprobación del modelo
Regla de inferencia
Propiedad de seguridad
Flujo de entrada
Obligación de prueba
Model Check
Inference Rule
Safety Property
Input Stream
Proof Obligation
dc.subject.proposal.eng.fl_str_mv Model Check
Inference Rule
Safety Property
Input Stream
Proof Obligation
description The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a formula to inductive properties of the underlying equational theory by means of the application of a few inference rules. Through the combination of various techniques such as unification, narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation, verifying automatically many proof obligations. Maude Inductive Theorem Prover (ITP) can be used to discharge the remaining obligations which are not automatically verified by InvA. Verification of the reliable communication ensured by the Alternating Bit Protocol (ABP) is used as a case study to explain the use of the InvA tool, and to illustrate its effectiveness and degree of automation in a concrete way.
publishDate 2014
dc.date.issued.none.fl_str_mv 2014
dc.date.accessioned.none.fl_str_mv 2021-12-01T20:41:59Z
dc.date.available.none.fl_str_mv 2021-12-01T20:41:59Z
dc.type.spa.fl_str_mv Capítulo - Parte de Libro
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.version.spa.fl_str_mv info:eu-repo/semantics/publishedVersion
dc.type.coar.spa.fl_str_mv http://purl.org/coar/resource_type/c_3248
dc.type.content.spa.fl_str_mv Text
dc.type.driver.spa.fl_str_mv info:eu-repo/semantics/bookPart
dc.type.redcol.spa.fl_str_mv http://purl.org/redcol/resource_type/ART
format http://purl.org/coar/resource_type/c_3248
status_str publishedVersion
dc.identifier.isbn.none.fl_str_mv 9783642546242
9783642546235
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/1882
identifier_str_mv 9783642546242
9783642546235
url https://repositorio.escuelaing.edu.co/handle/001/1882
dc.language.iso.spa.fl_str_mv eng
language eng
dc.relation.ispartofseries.none.fl_str_mv Lecture Notes in Computer Science;8373
dc.relation.citationendpage.spa.fl_str_mv 629
dc.relation.citationstartpage.spa.fl_str_mv 603
dc.relation.indexed.spa.fl_str_mv N/A
dc.relation.ispartofbook.eng.fl_str_mv Specification, Algebra, and Software
dc.relation.references.spa.fl_str_mv Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Eindhoven, The Netherlands, June 24-26. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commununications of the ACM 12(5), 260–261 (1969)
Bergstra, J., Klop, J.: Verification of an Alternating Bit Protocol by means of process algebra protocol. In: Bibel, W., Jantke, K. (eds.) Mathematical Methods of Specification and Synthesis of Software Systems 1985. LNCS, vol. 215, pp. 9–23. Springer, Heidelberg (1986)
Bezem, M., Groote, J.F.: Invariants in process algebra with data. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 401–416. Springer, Heidelberg (1994)
Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Clavel, M., Egea, M.: ITP/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 368–373. Springer, Heidelberg (2006)
Durán, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010)
Futatsugi, K., Gâinâ, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theoretical Computer Science 464, 90–112 (2012)
Găină, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R. (ed.) CALCO 2013. LNCS, vol. 8089, pp. 328–333. Springer, Heidelberg (2013)
Giménez, E.: An application of co-inductive types in Coq: Verification of the Alternating Bit Protocol. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 135–152. Springer, Heidelberg (1996)
Gutiérrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 162–181. Springer, Heidelberg (2012)
Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)
Lin, K., Goguen, J.: A hidden proof of the Alternating Bit Protocol,
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Meseguer, J.: Twenty years of rewriting logic. JLAP 81(7-8), 721–781 (2012)
Meseguer, J., Goguen, J.A.: Initially, induction and computability. Algebraic Methods in Semantics (1986)
Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Crème: an automatic invariant prover of behavioral specifications. International Journal of Software Engineering and Knowledge Engineering 17(6), 783–804 (2007)
Ogata, K., Futatsugi, K.: Proof scores in the OTS/CafeOBJ Method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)
Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS/CafeOBJ method. Electronic Notes in Theorethical Computer Science 201, 127–154 (2008)
Ogata, K., Futatsugi, K.: Proof score approach to analysis of electronic commerce protocols. International Journal of Software Engineering and Knowledge Engineering 20(2), 253–287 (2010)|
Pnueli, A.: Deduction is forever (1999) Invited talk at FM 1999 avaliable online at cs.nyu.edu/pnueli/fm99.ps
Rocha, C.: Symbolic Reachability Analysis for Rewrite Theories. PhD thesis, University of Illinois at Urbana-Champaign (2012), http://hdl.handle.net/2142/42200
Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314–328. Springer, Heidelberg (2011)
Roşu, G., Ştefănescu, A.: Matching Logic: A New Program Verification Approach (NIER Track). In: ICSE 211: Proceedings of the 30th International Conference on Software Engineering, pp. 868–871. ACM (2011)
Steggles, L., Kosiuczenko, P.: A timed rewriting logic semantics for SDL: A case study of the Alternating Bit Protocol. Electronic Notes in Theoretical Computer Science 15, 83–104 (1998)
Suzuki, I.: Formal analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering 16(11), 1273–1281 (1990)
Viry, P.: Equational rules for rewriting logic. TCS 285, 487–517 (2002)
dc.rights.eng.fl_str_mv © Springer-Verlag Berlin Heidelberg 2014
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_14cb
dc.rights.uri.spa.fl_str_mv https://creativecommons.org/licenses/by/4.0/
dc.rights.accessrights.spa.fl_str_mv info:eu-repo/semantics/closedAccess
dc.rights.creativecommons.spa.fl_str_mv Atribución 4.0 Internacional (CC BY 4.0)
rights_invalid_str_mv © Springer-Verlag Berlin Heidelberg 2014
https://creativecommons.org/licenses/by/4.0/
Atribución 4.0 Internacional (CC BY 4.0)
http://purl.org/coar/access_right/c_14cb
eu_rights_str_mv closedAccess
dc.format.extent.spa.fl_str_mv 27 páginas.
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.spa.fl_str_mv Springer.
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/1882/1/Mechanical%20Analysis%20of%20Reliable%20Communication%20in%20the%20Alternating%20Bit%20Protocol%20Using%20the%20Maude%20Invariant%20Analyzer%20Tool.png
https://repositorio.escuelaing.edu.co/bitstream/001/1882/2/license.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1882/3/SPRINGER-660x220.png.jpg
https://repositorio.escuelaing.edu.co/bitstream/001/1882/4/Mechanical%20Analysis%20of%20Reliable%20Communication%20in%20the%20Alternating%20Bit%20Protocol%20Using%20the%20Maude%20Invariant%20Analyzer%20Tool.png.jpg
bitstream.checksum.fl_str_mv b28fadbd3a62d439751fefaa4b41c7a0
5a7ca94c2e5326ee169f979d71d0f06e
b3cfb2d465b6323eedfaa1eb3a39827d
b3cfb2d465b6323eedfaa1eb3a39827d
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
MD5
MD5
repository.name.fl_str_mv Repositorio Escuela Colombiana de Ingeniería Julio Garavito
repository.mail.fl_str_mv repositorio.eci@escuelaing.edu.co
_version_ 1814355617155907584
spelling Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Meseguer, José6da02984a567cfba226ed9b8bf7c47c0600Informática2021-12-01T20:41:59Z2021-12-01T20:41:59Z201497836425462429783642546235https://repositorio.escuelaing.edu.co/handle/001/1882The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a formula to inductive properties of the underlying equational theory by means of the application of a few inference rules. Through the combination of various techniques such as unification, narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation, verifying automatically many proof obligations. Maude Inductive Theorem Prover (ITP) can be used to discharge the remaining obligations which are not automatically verified by InvA. Verification of the reliable communication ensured by the Alternating Bit Protocol (ABP) is used as a case study to explain the use of the InvA tool, and to illustrate its effectiveness and degree of automation in a concrete way.La herramienta InvA admite la verificación deductiva de las propiedades de seguridad de los sistemas concurrentes de estado infinito. Dado un sistema concurrente especificado como una teoría de reescritura y una fórmula de seguridad a verificar, InvA reduce dicha fórmula a las propiedades inductivas de la teoría ecuacional subyacente mediante la aplicación de algunas reglas de inferencia. A través de la combinación de varias técnicas, como la unificación, el estrechamiento, los predicados de igualdad definidos por ecuaciones y la resolución SMT, InvA logra un grado significativo de automatización, verificando automáticamente muchas obligaciones de prueba. El probador del teorema inductivo de Maude (ITP) se puede utilizar para cumplir con las obligaciones restantes que InvA no verifica automáticamente. La verificación de la comunicación confiable asegurada por el Alternating Bit Protocol (ABP) se utiliza como caso de estudio para explicar el uso de la herramienta InvA, y para ilustrar su efectividad y grado de automatización de manera concreta.27 páginas.application/pdfengSpringer.Lecture Notes in Computer Science;8373629603N/ASpecification, Algebra, and SoftwareBae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Eindhoven, The Netherlands, June 24-26. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commununications of the ACM 12(5), 260–261 (1969)Bergstra, J., Klop, J.: Verification of an Alternating Bit Protocol by means of process algebra protocol. In: Bibel, W., Jantke, K. (eds.) Mathematical Methods of Specification and Synthesis of Software Systems 1985. LNCS, vol. 215, pp. 9–23. Springer, Heidelberg (1986)Bezem, M., Groote, J.F.: Invariants in process algebra with data. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 401–416. Springer, Heidelberg (1994)Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Clavel, M., Egea, M.: ITP/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 368–373. Springer, Heidelberg (2006)Durán, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010)Futatsugi, K., Gâinâ, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theoretical Computer Science 464, 90–112 (2012)Găină, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R. (ed.) CALCO 2013. LNCS, vol. 8089, pp. 328–333. Springer, Heidelberg (2013)Giménez, E.: An application of co-inductive types in Coq: Verification of the Alternating Bit Protocol. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 135–152. Springer, Heidelberg (1996)Gutiérrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 162–181. Springer, Heidelberg (2012)Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)Lin, K., Goguen, J.: A hidden proof of the Alternating Bit Protocol,Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)Meseguer, J.: Twenty years of rewriting logic. JLAP 81(7-8), 721–781 (2012)Meseguer, J., Goguen, J.A.: Initially, induction and computability. Algebraic Methods in Semantics (1986)Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Crème: an automatic invariant prover of behavioral specifications. International Journal of Software Engineering and Knowledge Engineering 17(6), 783–804 (2007)Ogata, K., Futatsugi, K.: Proof scores in the OTS/CafeOBJ Method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS/CafeOBJ method. Electronic Notes in Theorethical Computer Science 201, 127–154 (2008)Ogata, K., Futatsugi, K.: Proof score approach to analysis of electronic commerce protocols. International Journal of Software Engineering and Knowledge Engineering 20(2), 253–287 (2010)|Pnueli, A.: Deduction is forever (1999) Invited talk at FM 1999 avaliable online at cs.nyu.edu/pnueli/fm99.psRocha, C.: Symbolic Reachability Analysis for Rewrite Theories. PhD thesis, University of Illinois at Urbana-Champaign (2012), http://hdl.handle.net/2142/42200Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314–328. Springer, Heidelberg (2011)Roşu, G., Ştefănescu, A.: Matching Logic: A New Program Verification Approach (NIER Track). In: ICSE 211: Proceedings of the 30th International Conference on Software Engineering, pp. 868–871. ACM (2011)Steggles, L., Kosiuczenko, P.: A timed rewriting logic semantics for SDL: A case study of the Alternating Bit Protocol. Electronic Notes in Theoretical Computer Science 15, 83–104 (1998)Suzuki, I.: Formal analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering 16(11), 1273–1281 (1990)Viry, P.: Equational rules for rewriting logic. TCS 285, 487–517 (2002)© Springer-Verlag Berlin Heidelberg 2014https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/closedAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_14cbMechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer ToolCapítulo - Parte de Libroinfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85Comprobación del modeloRegla de inferenciaPropiedad de seguridadFlujo de entradaObligación de pruebaModel CheckInference RuleSafety PropertyInput StreamProof ObligationORIGINALMechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool.pngMechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool.pngimage/png29134https://repositorio.escuelaing.edu.co/bitstream/001/1882/1/Mechanical%20Analysis%20of%20Reliable%20Communication%20in%20the%20Alternating%20Bit%20Protocol%20Using%20the%20Maude%20Invariant%20Analyzer%20Tool.pngb28fadbd3a62d439751fefaa4b41c7a0MD51metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1882/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTHUMBNAILSPRINGER-660x220.png.jpgSPRINGER-660x220.png.jpgGenerated Thumbnailimage/jpeg4164https://repositorio.escuelaing.edu.co/bitstream/001/1882/3/SPRINGER-660x220.png.jpgb3cfb2d465b6323eedfaa1eb3a39827dMD53open accessMechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool.png.jpgMechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool.png.jpgGenerated Thumbnailimage/jpeg4164https://repositorio.escuelaing.edu.co/bitstream/001/1882/4/Mechanical%20Analysis%20of%20Reliable%20Communication%20in%20the%20Alternating%20Bit%20Protocol%20Using%20the%20Maude%20Invariant%20Analyzer%20Tool.png.jpgb3cfb2d465b6323eedfaa1eb3a39827dMD54metadata only access001/1882oai:repositorio.escuelaing.edu.co:001/18822022-07-17 03:02:18.7metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK

Publicaciones similares