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

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