{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:02:34Z","timestamp":1779087754383,"version":"3.51.4"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319686899","type":"print"},{"value":"9783319686905","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68690-5_18","type":"book-chapter","created":{"date-parts":[[2017,10,9]],"date-time":"2017-10-09T21:14:51Z","timestamp":1507583691000},"page":"298-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Exploring Design Alternatives for RAMP Transactions Through Statistical Model\u00a0Checking"],"prefix":"10.1007","author":[{"given":"Si","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jatin","family":"Ganhotra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Indranil","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,10,11]]},"reference":[{"key":"18_CR1","unstructured":"PRISM. \n                      http:\/\/www.prismmodelchecker.org\/"},{"key":"18_CR2","unstructured":"Uppaal SMC. \n                      http:\/\/people.cs.aau.dk\/adavid\/smc\/"},{"issue":"2","key":"18_CR3","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"GA Agha","year":"2006","unstructured":"Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2), 213\u2013239 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011). doi:\n                      10.1007\/978-3-642-22944-2_28"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Bailis, P., Fekete, A., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Scalable atomic visibility with RAMP transactions. ACM Trans. Database Syst. 41(3) (2016)","DOI":"10.1145\/2909870"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bailis, P., Fekete, A., Hellerstein, J.M., Ghodsi, A., Stoica, I.: Scalable atomic visibility with RAMP transactions. In: Proceedings SIGMOD 2014. ACM (2014)","DOI":"10.1145\/2588555.2588562"},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1016\/j.future.2013.12.036","volume":"37","author":"E Barbierato","year":"2014","unstructured":"Barbierato, E., Gribaudo, M., Iacono, M.: Performance evaluation of NoSQL big-data applications using multi-formalism models. Future Gen. Comp. Syst. 37, 345\u2013353 (2014)","journal-title":"Future Gen. Comp. Syst."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Benson, T., Akella, A., Maltz, D.A.: Network traffic characteristics of data centers in the wild. In: IMC, pp. 267\u2013280 (2010)","DOI":"10.1145\/1879141.1879175"},{"key":"18_CR9","series-title":"LNCS","volume-title":"All About Maude","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-10885-8_2","volume-title":"Computer Performance Engineering","author":"A Gandini","year":"2014","unstructured":"Gandini, A., Gribaudo, M., Knottenbelt, W.J., Osman, R., Piazzolla, P.: Performance evaluation of NoSQL databases. In: Horv\u00e1th, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 16\u201329. Springer, Cham (2014). doi:\n                      10.1007\/978-3-319-10885-8_2"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/978-3-642-54624-2_25","volume-title":"Specification, Algebra, and Software","author":"J Grov","year":"2014","unstructured":"Grov, J., \u00d6lveczky, P.C.: Formal modeling and analysis of Google\u2019s Megastore in Real-Time Maude. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 494\u2013519. Springer, Heidelberg (2014). doi:\n                      10.1007\/978-3-642-54624-2_25"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-319-10431-7_12","volume-title":"Software Engineering and Formal Methods","author":"J Grov","year":"2014","unstructured":"Grov, J., \u00d6lveczky, P.C.: Increasing consistency in multi-site data stores: Megastore-CGC and its formal analysis. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 159\u2013174. Springer, Cham (2014). doi:\n                      10.1007\/978-3-319-10431-7_12"},{"issue":"1","key":"18_CR13","first-page":"031","volume":"4","author":"S Liu","year":"2017","unstructured":"Liu, S., Ganhotra, J., Rahman, M., Nguyen, S., Gupta, I., Meseguer, J.: Quantitative analysis of consistency in NoSQL key-value stores. Leibniz Trans. Embed. Syst. 4(1), 031\u20130326 (2017)","journal-title":"Leibniz Trans. Embed. Syst."},{"key":"18_CR14","unstructured":"Liu, S., \u00d6lveczky, P.C., Ganhotra, J., Gupta, I., Meseguer, J.: Exploring design alternatives for RAMP transactions through statistical model checking. Technical report (2017). \n                      https:\/\/sites.google.com\/site\/siliunobi\/ramp-smc"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Rahman, M.R., Ganhotra, J., Gupta, I., Meseguer, J.: Formal modeling and analysis of RAMP transaction systems. In: SAC. ACM (2016)","DOI":"10.1145\/2851613.2851838"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-319-11737-9_22","volume-title":"Formal Methods and Software Engineering","author":"S Liu","year":"2014","unstructured":"Liu, S., Rahman, M.R., Skeirik, S., Gupta, I., Meseguer, J.: Formal modeling and analysis of Cassandra in Maude. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 332\u2013347. Springer, Cham (2014). doi:\n                      10.1007\/978-3-319-11737-9_22"},{"issue":"1","key":"18_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266\u2013280. Springer, Heidelberg (2005). doi:\n                      10.1007\/11513988_26"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST 2005. IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.42"},{"issue":"9","key":"18_CR20","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368\u20131409 (2006)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68690-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:53:58Z","timestamp":1558320838000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68690-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319686899","9783319686905"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68690-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"11 October 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Xi'an","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 November 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ictt.xidian.edu.cn\/icfem2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}