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é
N1 - Publisher Copyright:
© 2017, Springer International Publishing AG.
PY - 2017
Y1 - 2017
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
T2 - 19th International Conference on Formal Engineering Methods, ICFEM 2017
Y2 - 13 November 2017 through 17 November 2017
ER -