A theorem prover-based analysis tool for object-oriented databases

David Spelt, Susan Even

Research output: Contribution to conferencePaperAcademicpeer-review

67 Downloads (Pure)

Abstract

We present a theorem-prover based analysis tool for object-oriented database systems with integrity constraints. Object-oriented database specifications are mapped to higher-order logic (HOL). This allows us to reason about the semantics of database operations using a mechanical theorem prover such as Isabelle or PVS. The tool can be used to verify various semantics requirements of the schema (such as transaction safety, compensation, and commutativity) to support the advanced transaction models used in workflow and cooperative work. We give an example of method safety analysis for the generic structure editing operations of a cooperative authoring system.
Original languageEnglish
Pages375-389
Number of pages15
DOIs
Publication statusPublished - Mar 1999
Event5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 1999 - Amsterdam, Netherlands
Duration: 22 Mar 199928 Mar 1999
Conference number: 5

Conference

Conference5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 1999
Abbreviated titleTACAS
CountryNetherlands
CityAmsterdam
Period22/03/9928/03/99

Keywords

  • DB-OODB: OBJECT-ORIENTED DATABASES
  • Integrity constraint
  • Database schemas
  • Database transactions
  • Schema translator
  • Object store

Fingerprint Dive into the research topics of 'A theorem prover-based analysis tool for object-oriented databases'. Together they form a unique fingerprint.

Cite this