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 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átic