Advertisement
Published in:
2017 | OriginalPaper | Chapter
Formal Modelling and Analysis of Distributed Storage Systems
Authors : Jordan de la Houssaye, Franck Pommereau, Philippe Deniel
Published in: Transactions on Petri Nets and Other Models of Concurrency XII
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
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.