Compensation methods to support generic graph editing: A case study in automated verification of schema requirements for an advanced transaction model

S.J. Even, D. Spelt

Research output: Contribution to conferencePaperAcademicpeer-review

83 Downloads (Pure)


Compensation plays an important role in advanced transaction models, cooperative work, and workflow systems. However, compensation operations are often simply written as a^−1 in transaction model literature. This notation ignores any operation parameters, results, and side effects. A schema designer intending to use an advanced transaction model is expected (required) to write correct method code. However, in the days of cut-and-paste, this is much easier said than done. In this paper, we demonstrate the feasibility of using an off-the-shelf theorem prover (also called a proof assistant) to perform automated verification of compensation requirements for an OODB schema. We report on the results of a case study in verification for a particular advanced transaction model that supports cooperative applications. The case study is based on an OODB schema that provides generic graph editing functionality for the creation, insertion, and manipulation of nodes and links.
Original languageUndefined
Number of pages12
Publication statusPublished - Jun 1999
Event1st ECOOP Workshop on Object-Oriented Databases - Lisbon, Portugal
Duration: 15 Jun 199915 Jun 1999


Workshop1st ECOOP Workshop on Object-Oriented Databases
Other15 Jun 1999


  • EWI-7211
  • IR-66433

Cite this