Mechanical Verification of Transaction Processing Systems
and Peter van der Stok
Appeared in: Proceedings 3th International Conference on
Formal Engineering Methods (ICFEM 2000), IEEE, pages 89-97, 2000.
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, 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 proved with the interactive proof checker of
that our system satisfies atomicity, durability
and serializability properties.
PVS dump file