Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 3 / Issue 4

available in:   PDF (311 kB) PS (93 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-003-04-0320


Formalizing Database Recovery

Yuri Gurevich (University of Michigan, USA)

Nandit Soparkar (University of Michigan, USA)

Charles Wallace (University of Michigan, USA)

Abstract: Failure resilience is an essential requirement for database systems, yet there has been little effort to specify and verify techniques for failure recovery formally. The desire to improve performance has resulted in algorithms of considerable sophistication, yet understood by few and prone to errors. In this paper, we illustrate how the methodology of Gurevich Abstract State Machines can elucidate recovery and provide formal rigor to the design of a recovery algorithm. In a series of refinements, we model a recovery algorithm at several levels of abstraction, verifying the correctness of each model. This work suggests that our approach can be applied to more advanced recovery mechanisms.