Verification of a distributed cache memory by using abstractions

Abstract

The purpose of this paper is to verify a distributed cache memory system by using the following general verification method: verify the properties characterizing a complex system on some small finite abstraction of it, obtained as a composition of abstractions of each component of the system. For a large class of systems including infinite state systems, the abstractions of the components can be obtained by replacing all operators on concrete domains by abstract operators on some abstract domain. This holds also for the abstraction of the control part of the system as we consider a kind of guarded command programs where all the control is expressed in terms of operations on explicit control variables.