Back to University of Twente portal
Verification Support for Object Database Design
Spelt, David (1999) Verification Support for Object Database Design. thesis.
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| 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 |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page
Metis ID: 118427