Formal modeling and analysis of cassandra in maude

S. Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta, Jose Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings
EditorsStephan Merz, Jun Pang
PublisherSpringer-Verlag
Pages332-347
Number of pages16
ISBN (Electronic)9783319117362
StatePublished - Jan 1 2014
Event16th International Conference on Formal Engineering Methods, ICFEM 2014 - Luxembourg, Luxembourg
Duration: Nov 3 2014Nov 5 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8829
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other16th International Conference on Formal Engineering Methods, ICFEM 2014
CountryLuxembourg
CityLuxembourg
Period11/3/1411/5/14

Fingerprint

Maude
Formal Modeling
Formal Analysis
Latency
Formal Model
Communication
Cloud computing
Cloud Computing
Model

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Liu, S., Rahman, M. R., Skeirik, S., Gupta, I., & Meseguer, J. (2014). Formal modeling and analysis of cassandra in maude. In S. Merz, & J. Pang (Eds.), Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings (pp. 332-347). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8829). Springer-Verlag.

Formal modeling and analysis of cassandra in maude. / Liu, S.; Rahman, Muntasir Raihan; Skeirik, Stephen; Gupta, Indranil; Meseguer, Jose.

Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings. ed. / Stephan Merz; Jun Pang. Springer-Verlag, 2014. p. 332-347 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8829).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Liu, S, Rahman, MR, Skeirik, S, Gupta, I & Meseguer, J 2014, Formal modeling and analysis of cassandra in maude. in S Merz & J Pang (eds), Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8829, Springer-Verlag, pp. 332-347, 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, 11/3/14.
Liu S, Rahman MR, Skeirik S, Gupta I, Meseguer J. Formal modeling and analysis of cassandra in maude. In Merz S, Pang J, editors, Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings. Springer-Verlag. 2014. p. 332-347. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Liu, S. ; Rahman, Muntasir Raihan ; Skeirik, Stephen ; Gupta, Indranil ; Meseguer, Jose. / Formal modeling and analysis of cassandra in maude. Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings. editor / Stephan Merz ; Jun Pang. Springer-Verlag, 2014. pp. 332-347 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{1006afc718194e65b3ee89e404be0669,
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.",
author = "S. Liu and Rahman, {Muntasir Raihan} and Stephen Skeirik and Indranil Gupta and Jose Meseguer",
year = "2014",
month = "1",
day = "1",
language = "English (US)",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "332--347",
editor = "Stephan Merz and Jun Pang",
booktitle = "Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings",

}

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, Jose

PY - 2014/1/1

Y1 - 2014/1/1

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

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-Verlag

ER -