Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking

Si Liu, Peter Csaba Ölveczky, Jatin Ganhotra, Indranil Gupta, José Meseguer

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

Abstract

Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings
EditorsZhenhua Duan, Luke Ong
PublisherSpringer-Verlag
Pages298-314
Number of pages17
ISBN (Print)9783319686899
DOIs
StatePublished - Jan 1 2017
Event19th International Conference on Formal Engineering Methods, ICFEM 2017 - Xi'an, China
Duration: Nov 13 2017Nov 17 2017

Publication series

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

Other

Other19th International Conference on Formal Engineering Methods, ICFEM 2017
CountryChina
CityXi'an
Period11/13/1711/17/17

Fingerprint

Model checking
Model Checking
Statistical Model
Transactions
Partition
Alternatives
Maude
Formal Modeling
Experimental Validation
Experimental Evaluation
System Design
Design
Statistical Models
Distributed Systems
Systems analysis
Personnel

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Liu, S., Ölveczky, P. C., Ganhotra, J., Gupta, I., & Meseguer, J. (2017). Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking. In Z. Duan, & L. Ong (Eds.), Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings (pp. 298-314). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10610 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-68690-5_18

Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking. / Liu, Si; Ölveczky, Peter Csaba; Ganhotra, Jatin; Gupta, Indranil; Meseguer, José.

Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings. ed. / Zhenhua Duan; Luke Ong. Springer-Verlag, 2017. p. 298-314 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10610 LNCS).

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

Liu, S, Ölveczky, PC, Ganhotra, J, Gupta, I & Meseguer, J 2017, Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking. in Z Duan & L Ong (eds), Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10610 LNCS, Springer-Verlag, pp. 298-314, 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, 11/13/17. https://doi.org/10.1007/978-3-319-68690-5_18
Liu S, Ölveczky PC, Ganhotra J, Gupta I, Meseguer J. Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking. In Duan Z, Ong L, editors, Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings. Springer-Verlag. 2017. p. 298-314. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-68690-5_18
Liu, Si ; Ölveczky, Peter Csaba ; Ganhotra, Jatin ; Gupta, Indranil ; Meseguer, José. / Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking. Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings. editor / Zhenhua Duan ; Luke Ong. Springer-Verlag, 2017. pp. 298-314 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f9271726fc1343eaba3df9262aab3a5d,
title = "Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking",
abstract = "Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.",
author = "Si Liu and {\"O}lveczky, {Peter Csaba} and Jatin Ganhotra and Indranil Gupta and Jos{\'e} Meseguer",
year = "2017",
month = "1",
day = "1",
doi = "10.1007/978-3-319-68690-5_18",
language = "English (US)",
isbn = "9783319686899",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "298--314",
editor = "Zhenhua Duan and Luke Ong",
booktitle = "Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings",

}

TY - GEN

T1 - Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking

AU - Liu, Si

AU - Ölveczky, Peter Csaba

AU - Ganhotra, Jatin

AU - Gupta, Indranil

AU - Meseguer, José

PY - 2017/1/1

Y1 - 2017/1/1

N2 - Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.

AB - Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.

UR - http://www.scopus.com/inward/record.url?scp=85032511338&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85032511338&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-68690-5_18

DO - 10.1007/978-3-319-68690-5_18

M3 - Conference contribution

AN - SCOPUS:85032511338

SN - 9783319686899

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 298

EP - 314

BT - Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings

A2 - Duan, Zhenhua

A2 - Ong, Luke

PB - Springer-Verlag

ER -