Model and verification of a data manager based on ARIES.
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.
| Xuất bản năm: | ACM transactions on database systems. 21, 4 (1996). |
|---|---|
| Tác giả chính: | |
| Định dạng: | Bài viết |
| Ngôn ngữ: | English |
| Những chủ đề: |