Talk "Design and Validation of Cloud Storage Systems using Rewriting Logic"

by Peter Ölveczky

Sat, 06 April 2019 at 05:13 pm in Prague, Czech Republic

Joint work with: Si Liu, Jose Meseguer, and others

Abstract: To deal with large amounts of data while offering high availability and throughput and low latency, cloud computing systems rely on distributed, partitioned, and replicated data stores. Such cloud storage systems are complex software artifacts that are very hard to design and analyze, also because of the need to analyze both correctness and performance. Within the context of the University of Illinois' Assured Cloud Computing, we have used rewriting logic, its associated Maude tools, and the PVeStA statistical model checker to model and analyze both the correctness of a range of state-of-the-art industrial and academic data stores, including Apache Cassandra, Google's Megastore, and UC Berkeley's RAMP transactions. Furthermore, we have used a Maude-based methodology to design a new data store satisfying a new consistency property. This talk gives an overview of some of that work.