Formal Modelling and Analysis of Distributed Storage Systems.

Distributed storage systems are nowadays ubiquitous, very often under the form of a hierarchy of multiple caches. While a lot of effort has been dedicated to design, implement and optimise such systems, there exists to the best of our knowledge no attempt to use formal modelling and analysis in this field. This paper proposes a formal modelling framework to design distributed storage systems, with the innovating feature to separate the various concerns they involve like data-model, operations, policy, consistency, topology, etc. A model can then be analysed through model-checking to prove properties, or through simulation to assess its performance. In this paper, we define the framework and focus on performance analysis. We illustrate this on a simple yet realistic example, a LRU cache (least recently used, possibly the most known cache algorithm), showing that our proposal has the potential to be used to make design decisions before the real system is implemented.