Formalizing Database Recovery
- Yuri Gurevich ,
- Nandit Soparkar ,
- Charles Wallace
Springer J. of Universal Computer Science |
Failure resilience is an essential requirement for transaction-oriented 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, understood by few and prone to errors. In this paper, we show how the formal 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 recovery at several levels of abstraction, verifying the correctness of each model. This initial work indicates that our approach can be applied to more advanced recovery mechanisms.