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

D. Spelt, S.J. Even

Research output: Contribution to journalArticleAcademicpeer-review

132 Downloads (Pure)


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 another transaction to semantically undo the effects of . 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. It is shown how an OODB schema is translated to the language of the theorem prover so that proofs can be performed on the compensating transactions.
Original languageUndefined
Article number10.1002/cpe.610
Pages (from-to)1013-1032
Number of pages20
JournalConcurrency and computation
Issue number11
Publication statusPublished - Aug 2001


  • IR-65001
  • EWI-13507

Cite this