Tech Reports

ULCS-03-024

Temporal Deductive Verification of Cache Coherence Protocols

Michael Fisher and Alexei Lisitsa


Abstract

Firstorder temporal logics (FOTLs) are very expressive formalisms in which we can specify, at a very natural level of abstraction, (almost) any computational system, together with its correctness conditions. This makes FOTLs ideal for formally specifying both software and hardware systems. Unfortunately, the expressiveness of FOTL also means that such logics are typically highly undecidable. Consequently, the fully automated deductive verification of FOTL specifications is not, in general, possible.

Recently, however, a tractable fragment of FOTL was identified by Hodkinson, Wolter and Zakharyashev. This fragement, termed the monodic fragment is amenable to automated proof techniques, and we have developed a number of theorem-proving systems for this fragment. In this paper, we particularly consider the use of such tractable fragments of firstorder temporal logics in the deductive verification of an important class of protocols, namely cache coherence protocols. This is the first use of monodic FOTLs in the deductive verification of reactive systems.

[Full Paper]