TY - GEN
T1 - Formal modeling and analysis of cassandra in maude
AU - Liu, S.
AU - Rahman, Muntasir Raihan
AU - Skeirik, Stephen
AU - Gupta, Indranil
AU - Meseguer, José
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84908700327&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84908700327&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-11737-9_22
DO - 10.1007/978-3-319-11737-9_22
M3 - Conference contribution
AN - SCOPUS:84908700327
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 332
EP - 347
BT - Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings
A2 - Merz, Stephan
A2 - Pang, Jun
PB - Springer
T2 - 16th International Conference on Formal Engineering Methods, ICFEM 2014
Y2 - 3 November 2014 through 5 November 2014
ER -