Read atomic transactions with prevention of lost updates: ROLA and its formal analysis

DOI10.1007/S00165-019-00489-WMaRDI QIDQ2335948zbMATH OpenOpenAlexFDO

Authors Si Liu, Peter Csaba Ölveczky, Qi Wang, José Meseguer, Indranil Gupta

Publication date 18 November 2019

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2142/101836

zbMATH Keywords

performance evaluationstatistical model checkingrewriting logicMaudedistributed database systemstransaction protocolsconsistency models

Mathematics Subject Classification ID

Database theory (68P15) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• ROLA: a new distributed transaction protocol and its formal analysis
• scientific article; zbMATH DE number 97098
• A framework for transactional consistency models with atomic visibility
• Relaxing consistency requirement for read-only transactions
• Robustness against consistency models with atomic visibility

Cites work

• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• A framework for transactional consistency models with atomic visibility
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Computer Aided Verification
• Conditional rewriting logic as a unified model of concurrency
• Formalizing and validating the \(P\)-Store replicated data store in Maude
• Pascal's prism
• ROLA: a new distributed transaction protocol and its formal analysis
• Scalable atomic visibility with RAMP transactions
• Semantics and pragmatics of real-time maude
• Statistical model checking for composite actor systems
• Statistical probabilistic model checking with a focus on time-bounded properties

Cited in

(4)

• Automatic analysis of consistency properties of distributed transaction systems in Maude
• ROLA: a new distributed transaction protocol and its formal analysis
• Scalable atomic visibility with RAMP transactions
• Building correct-by-construction systems with formal patterns

Describes a project that uses

Uses Software

• PRISM
• Maude
• PMaude
• PVeStA
• VESTA
• MODIST
• SAMC
• IronFleet

This page was built for publication: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2335948)