Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model

摘要

Compensation plays an important role in advanced transaction models, cooperative work and workflow systems. A schema designer is typically required to supply for each transaction T another transaction T~-1 to semantically undo the effects of T. Little attention has been paid to the verification of the desirable properties of such operations, however. This paper demonstrates the use of a higher-order logic theorem prover for verifying that compensating transactions return a database to its original state.