Assured Cloud Computing

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

Rakesh Bobba¹, Jon Grov², Indranil Gupta³, Si Liu³, José Meseguer³, Peter Csaba Ölveczky^3,4, and Stephen Skeirik³

¹School of Electrical Engineering and Computer Science, Oregon State University, Corvallis, OR, USA

²Gauge AS, Oslo, Norway

³Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, USA

⁴Department of Informatics, University of Oslo, Oslo, Norway

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.

2.1 Introduction

Cloud computing relies on software systems that store large amounts of data correctly and efficiently. These cloud systems are ...