JUCS - Journal of Universal Computer Science 3(4): 320-340, doi: 10.3217/jucs-003-04-0320
Formalizing Database Recovery
expand article infoYuri Gurevich, Nandit Soparkar, Charles Wallace
‡ University of Michigan, United States of America
Open Access
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.