Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude

Rakesh Bobba, Jon Grov, Indranil Gupta, Si Liu, José Meseguer, Peter Csaba Ölveczky, Stephen Skeirik

Research output: Chapter in Book/Report/Conference proceedingChapter


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.
Original languageEnglish (US)
Title of host publicationAssured Cloud Computing
EditorsRoy H. Campbell, Charles A. Kamhoua, Kevin A. Kwiat
PublisherWiley-IEEE Press
ISBN (Electronic)9781119428497
ISBN (Print)9781119428633
StatePublished - Dec 20 2018


  • Amazon Web Services
  • read-atomic multipartition transaction systems
  • Maude tool
  • group key management
  • Google's Megastore
  • formal modeling
  • formal methods
  • cloud storage systems
  • Apache ZooKeeper
  • Apache Cassandra


Dive into the research topics of 'Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude'. Together they form a unique fingerprint.

Cite this