Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
Dmitri Chkliaev , Eindhoven University of Technology
Jozef Hooman , Eindhoven University of Technology
Peter van der Stok , University of Nijmegen
This paper concerns the formal specification and mechanical verification of transaction processing systems aimed at distributed databases. In such systems, a standard set of ACID properties must be ensured by a combination of concurrency control and recovery protocols. In the existing literature, these protocols are often studied in isolation, making strong assumptions about each other. The problem of combining them in a formal way is largely ignored. To study the formal verification of combined protocols, we specify a transaction processing system, integrating strict two-phase locking, undo/redo recovery and two-phase commit. In our method, state machines define the locking and undo/redo mechanism at distributed sites, whereas the interaction between sites according to the two-phase commit protocol is specified by assertions. We proved with the interactive proof checker of PVS that our system satisfies atomicity, durability and serializability properties.
J. Hooman, P. van der Stok and D. Chkliaev, "Mechanical Verification of Transaction Processing Systems," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 89.