Automatic Verification of Transactions on an Object-Oriented Database

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.

• Type: Conference
• Year: 1997
• Where: DBPL
• Authors: David Spelt, Herman Balsters
• Keywords: Data Model, Database, DBPL 1997, Isabelle Theorem Prover, Run-time Transaction Overhead