05663861

a

05663861 Kirchberg, Markus Schewe, Klaus-Dieter Zhao, Jane Using abstract state machines for the design of multi-level transaction schedulers. Abrial, Jean-Raymond (ed.) et al., Rigorous methods for software construction and analysis. Essays dedicated to Egon B\"orger on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-11446-5/pbk). Lecture Notes in Computer Science 5115, 65-77 (2009). 2009 Berlin: Springer EN

doi:10.1007/978-3-642-11447-2_5

Summary: Multi-level transactions have been suggested as an approach to increase transaction throughput in databases. The central idea is to enable some low-level conflicts to be ignored by taking higher-level application semantics into account. In this paper, we approach the formal specification of a multi-level transaction scheduler using Abstract State Machines. We are particularly interested in showing that concrete protocols for multi-level transaction processing arise as refinements of an abstract ground model specification. Furthermore, we are interested in the proof of desirable properties of such schedulers such as the correctness and if possible also completeness with respect to serialisability, and the recoverability of the accepted schedules. For this we investigate a two-phase locking and a hybrid protocol.