Mechanical verification of transaction processing systems

Concerns the formal specification and mechanical verification of transaction processing systems aimed at distributed databases. In such systems, a standard set of ACID (Atomicity, Consistency, Isolation and Durability) 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 has been 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, the locking and undo/redo mechanism at distributed sites is defined by state machines, whereas the interaction between sites according to the two-phase commit protocol is specified by assertions. We have proved, using the interactive proof checker of PVS, that our system satisfies atomicity, durability and serializability properties