title = { Characterization of a sequentially consistent memory and verification of a cache memory by abstraction },
    author = {Graf, Susanne},
    year = {1999},
    note = {accepted for publication without any further revision since 1995},
    journal = {Distributed Computing},
    publisher = {Springer Verlag},
    volume = {12},
    team = {DCS},
    abstract = {The contribution of the paper is two-fold. We give a set of properties expressible as temporal logic formulas such that any system satisfying them is a sequentially consistent memory, and which is sufficiently precise such that every reasonnable concrete system implementing a sequentially consistent memory satisfies these properties. Then, we verify these properties on a particular distributed cache memory systems by means of a verification method, based on the use of abstract interpretation which has been presented in previous papers (<A HREF=#LoiseauxGrafSifakisBouajjaniBensalem94> [LBBGS95]</A>) and often applied to finite state systems. The motivation of this paper was to show that it can also been applied to systems with infinite state space, and a more recent papers shows that the method can even be automatized (<A HREF=#GrafSaidi97>[GS97]</A>). This paper is a revised and extended version of (<A HREF=#graf94>[Graf94]</A>). },


Publication Sections

Contact | Site Map | Site powered by SPIP 3.0.25 + AHUNTSIC [CC License]

info visites 778165