Verification Support For Object Database Design

David Spelt

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

10 Downloads (Pure)

Abstract

In this thesis we have developed a verification theory and a tool for the automated analysis of assertions about object-oriented database schemas. The approach is inspired by the work of [SS89] in which a theorem prover is used to automate the verification of invariants for transactions on a relational database. The work presented in this thesis deals with an object-oriented database and it discusses applications other than the analysis of database transaction safety. An important difference with the work of [SS89] is that we have used a general purpose higher-order logic (HOL) theorem prover, namely the Isabelle theorem prover [Pau94, Isa], rather than implementing our own specialized prover. Much previous research, including the work of [SS89], concerns fully automatic techniques (i.e., without the possibility of further interaction). These techniques are inheritly limited in scope ([BGL96]). The presented approach, combines automatic and interactive proof, where Isabelle’s automatic proof facilities are exploited to minimize the user’s effort to discharge proof obligations. The results demonstrate that today’s prover technology can indeed help in practical verification issues that arise in the design of databases.
Original languageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Apers, Peter Maria Gerardus, Supervisor
  • Balsters, H., Co-Supervisor
Award date10 Sep 1999
Place of PublicationEnschede
Publisher
Print ISBNs90-365135-53
Publication statusPublished - 10 Sep 1999

Fingerprint

Object-oriented databases

Keywords

  • DB-PRJTM: TWENTE-MILANO
  • EWI-6360
  • DB-OODB: OBJECT-ORIENTED DATABASES
  • IR-17908
  • METIS-118427

Cite this

Spelt, D. (1999). Verification Support For Object Database Design. Enschede: Universiteit Twente.
Spelt, David. / Verification Support For Object Database Design. Enschede : Universiteit Twente, 1999. 156 p.
@phdthesis{bdcabf2d766949c3883ac1a1f917f003,
title = "Verification Support For Object Database Design",
abstract = "In this thesis we have developed a verification theory and a tool for the automated analysis of assertions about object-oriented database schemas. The approach is inspired by the work of [SS89] in which a theorem prover is used to automate the verification of invariants for transactions on a relational database. The work presented in this thesis deals with an object-oriented database and it discusses applications other than the analysis of database transaction safety. An important difference with the work of [SS89] is that we have used a general purpose higher-order logic (HOL) theorem prover, namely the Isabelle theorem prover [Pau94, Isa], rather than implementing our own specialized prover. Much previous research, including the work of [SS89], concerns fully automatic techniques (i.e., without the possibility of further interaction). These techniques are inheritly limited in scope ([BGL96]). The presented approach, combines automatic and interactive proof, where Isabelle’s automatic proof facilities are exploited to minimize the user’s effort to discharge proof obligations. The results demonstrate that today’s prover technology can indeed help in practical verification issues that arise in the design of databases.",
keywords = "DB-PRJTM: TWENTE-MILANO, EWI-6360, DB-OODB: OBJECT-ORIENTED DATABASES, IR-17908, METIS-118427",
author = "David Spelt",
note = "Imported from EWI/DB PMS [db-utwente:phdt:0000001002]",
year = "1999",
month = "9",
day = "10",
language = "English",
isbn = "90-365135-53",
publisher = "Universiteit Twente",
school = "University of Twente",

}

Spelt, D 1999, 'Verification Support For Object Database Design', University of Twente, Enschede.

Verification Support For Object Database Design. / Spelt, David.

Enschede : Universiteit Twente, 1999. 156 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

TY - THES

T1 - Verification Support For Object Database Design

AU - Spelt, David

N1 - Imported from EWI/DB PMS [db-utwente:phdt:0000001002]

PY - 1999/9/10

Y1 - 1999/9/10

N2 - In this thesis we have developed a verification theory and a tool for the automated analysis of assertions about object-oriented database schemas. The approach is inspired by the work of [SS89] in which a theorem prover is used to automate the verification of invariants for transactions on a relational database. The work presented in this thesis deals with an object-oriented database and it discusses applications other than the analysis of database transaction safety. An important difference with the work of [SS89] is that we have used a general purpose higher-order logic (HOL) theorem prover, namely the Isabelle theorem prover [Pau94, Isa], rather than implementing our own specialized prover. Much previous research, including the work of [SS89], concerns fully automatic techniques (i.e., without the possibility of further interaction). These techniques are inheritly limited in scope ([BGL96]). The presented approach, combines automatic and interactive proof, where Isabelle’s automatic proof facilities are exploited to minimize the user’s effort to discharge proof obligations. The results demonstrate that today’s prover technology can indeed help in practical verification issues that arise in the design of databases.

AB - In this thesis we have developed a verification theory and a tool for the automated analysis of assertions about object-oriented database schemas. The approach is inspired by the work of [SS89] in which a theorem prover is used to automate the verification of invariants for transactions on a relational database. The work presented in this thesis deals with an object-oriented database and it discusses applications other than the analysis of database transaction safety. An important difference with the work of [SS89] is that we have used a general purpose higher-order logic (HOL) theorem prover, namely the Isabelle theorem prover [Pau94, Isa], rather than implementing our own specialized prover. Much previous research, including the work of [SS89], concerns fully automatic techniques (i.e., without the possibility of further interaction). These techniques are inheritly limited in scope ([BGL96]). The presented approach, combines automatic and interactive proof, where Isabelle’s automatic proof facilities are exploited to minimize the user’s effort to discharge proof obligations. The results demonstrate that today’s prover technology can indeed help in practical verification issues that arise in the design of databases.

KW - DB-PRJTM: TWENTE-MILANO

KW - EWI-6360

KW - DB-OODB: OBJECT-ORIENTED DATABASES

KW - IR-17908

KW - METIS-118427

M3 - PhD Thesis - Research UT, graduation UT

SN - 90-365135-53

PB - Universiteit Twente

CY - Enschede

ER -

Spelt D. Verification Support For Object Database Design. Enschede: Universiteit Twente, 1999. 156 p.