@inproceedings{da8ad72e7dd2474ea17b130cc0942006,
title = "Formal verification of safety properties for a cache coherence protocol",
abstract = "This paper presents a case study on the formal specification of a cache coherence protocol and the verification of some of its safety properties. Cache coherence refers to the consistency between the contents of a memory resource shared by many processes, that can have read and write access, and each local copy of the memory contents. The protocol presented in this paper is based on the ESI standard in which a central controller can grant exclusive and shared access to the memory, and also invalidate access to the memory. The formal specification of the protocol is presented as a rewriting logic theory and it is fully executable in the Maude system. The safety properties presented in this paper are linear temporal logic (LTL) formulas expressing invariants about mutual exclusion among the processes accessing the shared memory resource. By using Maude's search functionality and LTL model checker, some of these invariants can be proved automatically for a finite number of processes. This paper also presents an initial exploration on the mechanical verification of an invariant for any number of processes by means of deductive techniques based on inductive reasoning.",
author = "Sergio Ramirez and Camilo Rocha",
note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 10th Colombian Computing Conference, 10CCC 2015 ; Conference date: 21-09-2015 Through 25-09-2015",
year = "2015",
month = nov,
day = "20",
doi = "10.1109/ColumbianCC.2015.7333399",
language = "English",
series = "2015 10th Colombian Computing Conference, 10CCC 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "9--16",
editor = "Oscar Gonzalez and Mario Sanchez",
booktitle = "2015 10th Colombian Computing Conference, 10CCC 2015",
address = "United States",
}