Verification Support for Object Database Design


Share/Save/Bookmark

Spelt, David (1999) Verification Support for Object Database Design. thesis.

[img]
Preview
PDF
888Kb
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.
Item Type:Thesis
Research Group:
Link to this item:http://purl.utwente.nl/publications/17908
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 118427