Automatic verification of transactions on an object-oriented database

David Spelt, Herman Balsters

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

11 Citations (Scopus)
44 Downloads (Pure)

Abstract

In the context of the object-oriented data model, a compiletime approach is given that provides for a significant reduction of the amount of run-time transaction overhead due to integrity constraint checking. The higher-order logic Isabelle theorem prover is used to automatically prove which constraints might, or might not be violated by a given transaction in a manner analogous to the one used by Sheard and Stemple (1989) for the relational data model. A prototype transaction verification tool has been implemented, which automates the semantic mappings and generates proof goals for Isabelle. Test results are discussed to illustrate the effectiveness of our approach.
Original languageEnglish
Title of host publicationDatabase Programming Languages
Subtitle of host publication6th International Workshop, DBPL-6 Estes Park, Colorado, USA, August 18–20, 1997, Proceedings
EditorsSophie Cluet, Rick Hull
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages396-412
Number of pages17
ISBN (Electronic)1611-3349
ISBN (Print)0302-9743
DOIs
Publication statusPublished - 1998
Event6th International Workshop on Database Programming Languages, DBPL 1997 - Estes Park, United States
Duration: 18 Aug 199720 Aug 1997
Conference number: 6

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1369
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Workshop

Workshop6th International Workshop on Database Programming Languages, DBPL 1997
Abbreviated titleDBPL
CountryUnited States
CityEstes Park
Period18/08/9720/08/97

Keywords

  • DB-PRJTM: TWENTE-MILANO
  • DB-OODB: OBJECT-ORIENTED DATABASES
  • Transaction verification
  • Transaction semantics
  • Object-oriented databases

Fingerprint Dive into the research topics of 'Automatic verification of transactions on an object-oriented database'. Together they form a unique fingerprint.

Cite this