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...
- 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
Summary: | 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. |
---|