Especificación formal y verificación de invariantes para un protocolo de coherencia del caché

This document presents a case study in the specification and verification of invariants of a cache coherence protocol. This protocol is based on the ESI coordination technique based on exclusive or shared access to a resource. Invariant verification uses algorithmic and deductive analysis, and Maude...

Full description

Autores:
Ramirez Rico, Sergio Steven
Tipo de recurso:
Trabajo de grado de pregrado
Fecha de publicación:
2015
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
spa
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/216
Acceso en línea:
http://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=17655
https://repositorio.escuelaing.edu.co/handle/001/216
Palabra clave:
Matemáticas
Memoria Caché
Math
Rights
openAccess
License
Derechos Reservados - Escuela Colombiana de Ingeniería Julio Garavito
id ESCUELAIG2_459d7324771975a46169164bf02700f8
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/216
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.spa.fl_str_mv Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
title Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
spellingShingle Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
Matemáticas
Memoria Caché
Math
title_short Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
title_full Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
title_fullStr Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
title_full_unstemmed Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
title_sort Especificación formal y verificación de invariantes para un protocolo de coherencia del caché
dc.creator.fl_str_mv Ramirez Rico, Sergio Steven
dc.contributor.advisor.spa.fl_str_mv Rocha Niño, Hernan Camilo, (dir)
dc.contributor.author.spa.fl_str_mv Ramirez Rico, Sergio Steven
dc.subject.spa.fl_str_mv Matemáticas
Memoria Caché
topic Matemáticas
Memoria Caché
Math
dc.subject.keywords.spa.fl_str_mv Math
description This document presents a case study in the specification and verification of invariants of a cache coherence protocol. This protocol is based on the ESI coordination technique based on exclusive or shared access to a resource. Invariant verification uses algorithmic and deductive analysis, and Maude is used as the specification language and verification system.
publishDate 2015
dc.date.accessioned.spa.fl_str_mv 2015-06-17T16:53:05Z
dc.date.available.spa.fl_str_mv 2015-06-17T16:53:05Z
dc.date.issued.spa.fl_str_mv 2015
dc.date.accessioned.none.fl_str_mv 2021-10-01T16:52:41Z
dc.date.available.none.fl_str_mv 2021-10-01T16:52:41Z
dc.type.spa.fl_str_mv Trabajo de grado - Pregrado
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_7a1f
dc.type.content.spa.fl_str_mv Text
dc.type.driver.spa.fl_str_mv info:eu-repo/semantics/bachelorThesis
dc.type.redcol.spa.fl_str_mv http://purl.org/redcol/resource_type/TP
format http://purl.org/coar/resource_type/c_7a1f
status_str publishedVersion
dc.identifier.uri.spa.fl_str_mv http://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=17655
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/216
url http://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=17655
https://repositorio.escuelaing.edu.co/handle/001/216
dc.language.iso.spa.fl_str_mv spa
language spa
dc.rights.spa.fl_str_mv Derechos Reservados - Escuela Colombiana de Ingeniería Julio Garavito
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.uri.spa.fl_str_mv https://creativecommons.org/licenses/by-nc/4.0/
dc.rights.accessrights.spa.fl_str_mv info:eu-repo/semantics/openAccess
dc.rights.creativecommons.spa.fl_str_mv Atribución-NoComercial 4.0 Internacional (CC BY-NC 4.0)
rights_invalid_str_mv Derechos Reservados - Escuela Colombiana de Ingeniería Julio Garavito
https://creativecommons.org/licenses/by-nc/4.0/
Atribución-NoComercial 4.0 Internacional (CC BY-NC 4.0)
http://purl.org/coar/access_right/c_abf2
eu_rights_str_mv openAccess
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.spa.fl_str_mv Escuela Colombiana de Ingeniería Julio Garavito
dc.publisher.program.spa.fl_str_mv Matemáticas
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/216/1/Ramirez%20Rico%2c%20Sergio%20Steven%20-%202015.pdf
https://repositorio.escuelaing.edu.co/bitstream/001/216/2/license.txt
https://repositorio.escuelaing.edu.co/bitstream/001/216/3/GA-Matematicas-1075671646.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/216/7/Ramirez%20Rico%2c%20Sergio%20Steven%20-%202015.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/216/5/GA-Matematicas-1075671646.pdf.jpg
https://repositorio.escuelaing.edu.co/bitstream/001/216/8/Ramirez%20Rico%2c%20Sergio%20Steven%20-%202015.pdf.jpg
bitstream.checksum.fl_str_mv 880b93a044b477bd4764d2a82901b39e
9480849945fd70c1da11fa639db5a11c
aac4d82a5540ccaf4514b8bf7f33d4c3
2a52b89062e2b8bc3ad17ba6911da4f2
c739d74d24b60fb02b5b531ed3ee2dde
a7fc622e89f6aac67cdaa2dd4c733d10
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
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_ 1814355599292366848
spelling Rocha Niño, Hernan Camilo, (dir)99ebc0ff61cbd40fb0c218980ddbc11bRamirez Rico, Sergio Steven538b7dbbc725de226506f6c7d90118406002015-06-17T16:53:05Z2021-10-01T16:52:41Z2015-06-17T16:53:05Z2021-10-01T16:52:41Z2015http://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=17655https://repositorio.escuelaing.edu.co/handle/001/216This document presents a case study in the specification and verification of invariants of a cache coherence protocol. This protocol is based on the ESI coordination technique based on exclusive or shared access to a resource. Invariant verification uses algorithmic and deductive analysis, and Maude is used as the specification language and verification system.Este documento presenta un caso de estudio en la especificación y verificación de invariantes de un protocolo de coherencia del caché. Este protocolo está fundamentado en la técnica ESI de coordinación basada en acceso exclusivo o compartido a un recurso. La verificación de los invariantes utiliza análisis algorítmico y deductivo, y se emplea Maude como lenguaje de especificación y sistema de verificación.PregradoMatemáticoapplication/pdfspaEscuela Colombiana de Ingeniería Julio GaravitoMatemáticasDerechos Reservados - Escuela Colombiana de Ingeniería Julio Garavitohttps://creativecommons.org/licenses/by-nc/4.0/info:eu-repo/semantics/openAccessAtribución-NoComercial 4.0 Internacional (CC BY-NC 4.0)http://purl.org/coar/access_right/c_abf2MatemáticasMemoria CachéMathEspecificación formal y verificación de invariantes para un protocolo de coherencia del cachéTrabajo de grado - Pregradoinfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_7a1fTextinfo:eu-repo/semantics/bachelorThesishttp://purl.org/redcol/resource_type/TPhttp://purl.org/coar/version/c_970fb48d4fbd8a85ORIGINALRamirez Rico, Sergio Steven - 2015.pdfPDFapplication/pdf705877https://repositorio.escuelaing.edu.co/bitstream/001/216/1/Ramirez%20Rico%2c%20Sergio%20Steven%20-%202015.pdf880b93a044b477bd4764d2a82901b39eMD51open accessLICENSElicense.txttext/plain1762https://repositorio.escuelaing.edu.co/bitstream/001/216/2/license.txt9480849945fd70c1da11fa639db5a11cMD52open accessTEXTGA-Matematicas-1075671646.pdf.txtExtracted texttext/plain73530https://repositorio.escuelaing.edu.co/bitstream/001/216/3/GA-Matematicas-1075671646.pdf.txtaac4d82a5540ccaf4514b8bf7f33d4c3MD53open accessRamirez Rico, Sergio Steven - 2015.pdf.txtRamirez Rico, Sergio Steven - 2015.pdf.txtExtracted texttext/plain73533https://repositorio.escuelaing.edu.co/bitstream/001/216/7/Ramirez%20Rico%2c%20Sergio%20Steven%20-%202015.pdf.txt2a52b89062e2b8bc3ad17ba6911da4f2MD57open accessTHUMBNAILGA-Matematicas-1075671646.pdf.jpgIM Thumbnailimage/jpeg3290https://repositorio.escuelaing.edu.co/bitstream/001/216/5/GA-Matematicas-1075671646.pdf.jpgc739d74d24b60fb02b5b531ed3ee2ddeMD55open accessRamirez Rico, Sergio Steven - 2015.pdf.jpgRamirez Rico, Sergio Steven - 2015.pdf.jpgGenerated Thumbnailimage/jpeg6197https://repositorio.escuelaing.edu.co/bitstream/001/216/8/Ramirez%20Rico%2c%20Sergio%20Steven%20-%202015.pdf.jpga7fc622e89f6aac67cdaa2dd4c733d10MD58open access001/216oai:repositorio.escuelaing.edu.co:001/2162021-10-01 16:32:11.885open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCBjb25mZXJlbmNpYSwgbGlicm8sIGltYWdlbiwgZm90b2dyYWbDrWEsIGF1ZGlvLCBwcmVzZW50YWNpw7NuIHUgb3RybyAoZW4gYWRlbGFudGUgZG9jdW1lbnRvKSBxdWUgZW4gbGEgZmVjaGEgZW50cmVnbyBlbiBmb3JtYXRvIGRpZ2l0YWwsIHkgbGUgcGVybWl0byBkZSBmb3JtYSBpbmRlZmluaWRhIHF1ZSBsbyBwdWJsaXF1ZSBlbiBlbCByZXBvc2l0b3JpbyBpbnN0aXR1Y2lvbmFsLCBlbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZSBhbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIHVzbyBzb2JyZSBsYSBvYnJhIGVuIGZvcm1hdG8gZGlnaXRhbCwgZWxlY3Ryw7NuaWNvLCB2aXJ0dWFsOyB5IHBhcmEgdXNvcyBlbiByZWRlcywgaW50ZXJuZXQsIGV4dHJhbmV0LCB5IGN1YWxxdWllciBmb3JtYXRvIG8gbWVkaW8gY29ub2NpZG8gbyBwb3IgY29ub2Nlci4KRW4gbWkgY2FsaWRhZCBkZSBhdXRvciwgZXhwcmVzbyBxdWUgZWwgZG9jdW1lbnRvIG9iamV0byBkZSBsYSBwcmVzZW50ZSBhdXRvcml6YWNpw7NuIGVzIG9yaWdpbmFsIHkgbG8gZWxhYm9yw6kgc2luIHF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCB0ZW5nbyBsYSB0aXR1bGFyaWRhZCBzb2JyZSDDqWwuIEVuIGNhc28gZGUgcXVlamEgbyBhY2Npw7NuIHBvciBwYXJ0ZSBkZSB1biB0ZXJjZXJvIHJlZmVyZW50ZSBhIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBzb2JyZSBlbCBkb2N1bWVudG8gZW4gY3Vlc3Rpw7NuLCBhc3VtaXLDqSBsYSByZXNwb25zYWJpbGlkYWQgdG90YWwgeSBzYWxkcsOpIGVuIGRlZmVuc2EgZGUgbG9zIGRlcmVjaG9zIGFxdcOtIGF1dG9yaXphZG9zLiBFc3RvIHNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgcG9kcsOhIGNvcGlhciBhcGFydGVzIGRlbCB0ZXh0bywgY29uIGVsIGNvbXByb21pc28gZGUgY2l0YXIgc2llbXByZSBsYSBmdWVudGUsIGxhIGN1YWwgaW5jbHV5ZSBlbCB0w610dWxvIGRlbCB0cmFiYWpvIHkgZWwgYXV0b3IuIEVzdGEgYXV0b3JpemFjacOzbiBubyBpbXBsaWNhIHJlbnVuY2lhIGEgbGEgZmFjdWx0YWQgcXVlIHRlbmdvIGRlIHB1YmxpY2FyIHRvdGFsIG8gcGFyY2lhbG1lbnRlIGxhIG9icmEgZW4gb3Ryb3MgbWVkaW9zLiBFc3RhIGF1dG9yaXphY2nDs24gZXN0w6EgcmVzcGFsZGFkYSBwb3IgbGFzIGZpcm1hcyBkZWwgKGxvcykgYXV0b3IoZXMpIGRlbCBkb2N1bWVudG8uIApTw60gYXV0b3Jpem8gKGFtb3MpCg==

Publicaciones similares