Sciweavers

Share
DBPL
1997
Springer

Automatic Verification of Transactions on an Object-Oriented Database

9 years 1 months ago
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.
David Spelt, Herman Balsters
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1997
Where DBPL
Authors David Spelt, Herman Balsters
Comments (0)
books