Model and verification of a data manager based on ARIES
Dean Kuo · ACM Transactions on Database Systems · 1996
In this article, we model and verify a data manager whose algorithm is based on ARIES. The work uses the I/O automata method as the formal model and the definition of correctness is defined on the interface between the scheduler and the data manager.