Premium
Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model
Author(s) -
Spelt David,
Even Susan
Publication year - 2001
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.610
Subject(s) - computer science , undo , online transaction processing , schema (genetic algorithms) , database transaction , distributed transaction , programming language , database schema , transaction processing , workflow , database , automated theorem proving , software engineering , information retrieval , database design
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. 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. Copyright © 2001 John Wiley & Sons, Ltd.