University of Illinois Urbana-Champaign

Design, Formal Modeling, and Validation of Cloud Storage Systems using Maude

Bobba, Rakesh; Grov, Jon; Gupta, Indranil; Liu, Si; Meseguer, José; Olveczky, Peter C.; Skeirik, Stephen

Content Files
main.pdf

Permalink

https://hdl.handle.net/2142/96274

Description

Title
Design, Formal Modeling, and Validation of Cloud Storage Systems using Maude
Author(s)
  • Bobba, Rakesh
  • Grov, Jon
  • Gupta, Indranil
  • Liu, Si
  • Meseguer, José
  • Olveczky, Peter C.
  • Skeirik, Stephen
Issue Date
2017-06-28
Keyword(s)
  • cloud storage systems
  • distributed system design
  • formal modeling
  • formal analysis
  • Maude
Date of Ingest
2017-06-28T15:45:48Z
Abstract
To deal with large amounts of data while offering high availability, 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. We argue that formal specification and model checking analysis should significantly improve their design and validation. In particular, we propose rewriting logic and its accompanying Maude tools as a suitable framework for formally specifying and analyzing both the correctness and the performance of cloud storage systems. This chapter largely focuses on how we have used rewriting logic to model and analyze industrial cloud storage systems such as Google's Megastore, Apache Cassandra, Apache ZooKeeper, and RAMP. We also touch on the use of formal methods at Amazon Web Services.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/96274
Sponsor(s)/Grant Number(s)
This work is based on research sponsored by the Air Force Research Laboratory and the Air Force Office of Scientific Research, under agreement number FA8750-11-2-0084. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation thereon. This work is also based on research supported by the National Science Foundation under Grant Nos. NSF CNS 1409416 and NSF CNS 1319527.

Owning Collections

Research and Tech Reports - Computer Science PRIMARY