Abstract
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.
Original language | English |
---|---|
Pages | 375-389 |
Number of pages | 15 |
DOIs | |
Publication status | Published - Mar 1999 |
Event | 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 1999 - Amsterdam, Netherlands Duration: 22 Mar 1999 → 28 Mar 1999 Conference number: 5 |
Conference
Conference | 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 1999 |
---|---|
Abbreviated title | TACAS |
Country/Territory | Netherlands |
City | Amsterdam |
Period | 22/03/99 → 28/03/99 |
Keywords
- DB-OODB: OBJECT-ORIENTED DATABASES
- Integrity constraint
- Database schemas
- Database transactions
- Schema translator
- Object store