Sciweavers

TACAS
1999
Springer

A Theorem Prover-Based Analysis Tool for Object-Oriented Databases

13 years 8 months ago
A Theorem Prover-Based Analysis Tool for Object-Oriented Databases
We present a theorem-prover based analysis tool for object-oriented database systems with integrity constraints. Object-oriented database specifications are mapped to higher-order logic (HOL). This allows us to reason about the semantics of database operations using a mechanical theorem prover such as Isabelle or PVS. The tool can be used to verify various semantics requirements of the schema (such as transaction safety, compensation, and commutativity) to support the advanced transaction models used in workflow and cooperative work. We give an example of method safety analysis for the generic structure editing operations of a cooperative authoring system.
David Spelt, Susan Even
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1999
Where TACAS
Authors David Spelt, Susan Even
Comments (0)