Title
Formal Modeling and Analysis of Cassandra in Maude.
Abstract
Distributed key-value stores are quickly becoming a key component of cloud computing systems. In order to improve read/write latency, distributed key-value stores offer weak notions of consistency to clients by using many complex design decisions. However, it is challenging to formally analyze consistency behaviors of such systems, both because there are few formal models, and because different consistency level combinations render understanding hard, particularly under communication latency. This paper presents for the first time a formal executable model in Maude of Cassandra, a popular key-value store. We formally models Cassandra's main components and design strategies. We formally specify various consistency properties and model check them against our model under various communication latency and consistency combinations.
Year
DOI
Venue
2014
10.1007/978-3-319-11737-9_22
Lecture Notes in Computer Science
Field
DocType
Volume
Programming language,Latency (engineering),Cloud computing systems,Computer science,Real-time computing,Linear temporal logic,Global time,Consistency model,Strong consistency,Distributed computing,Executable
Conference
8829
ISSN
Citations 
PageRank 
0302-9743
9
0.54
References 
Authors
15
5
Name
Order
Citations
PageRank
Si Liu1424.43
Muntasir Raihan Rahman245521.21
Stephen Skeirik3293.27
Indranil Gupta41837143.92
José Meseguer59533805.39