A theorem prover-based analysis tool for object-oriented databases

David Spelt; Susan Even

doi:10.1007/3-540-49059-0_26

A theorem prover-based analysis tool for object-oriented databases

David Spelt, Susan Even

Databases (Former)

Research output: Contribution to conference › Paper › Academic › peer-review

67 Downloads (Pure)

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	https://doi.org/10.1007/3-540-49059-0_26
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

Access to Document

10.1007/3-540-49059-0_26

fulltext

Cite this

@conference{570e7e19c3804b50be4a9b05c13b3ea9,

title = "A theorem prover-based analysis tool for object-oriented databases",

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.",

keywords = "DB-OODB: OBJECT-ORIENTED DATABASES, Integrity constraint, Database schemas, Database transactions, Schema translator, Object store",

author = "David Spelt and Susan Even",

note = "Imported from EWI/DB PMS [db-utwente:inpr:0000003029], Part of: European Joint Conferences on Theory and Practice of Software (ETAPS'99), Amsterdam; 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 1999, TACAS ; Conference date: 22-03-1999 Through 28-03-1999",

year = "1999",

month = mar,

doi = "10.1007/3-540-49059-0_26",

language = "English",

pages = "375--389",

}

TY - CONF

T1 - A theorem prover-based analysis tool for object-oriented databases

AU - Spelt, David

AU - Even, Susan

N1 - Conference code: 5

PY - 1999/3

Y1 - 1999/3

N2 - 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.

AB - 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.

KW - DB-OODB: OBJECT-ORIENTED DATABASES

KW - Integrity constraint

KW - Database schemas

KW - Database transactions

KW - Schema translator

KW - Object store

U2 - 10.1007/3-540-49059-0_26

DO - 10.1007/3-540-49059-0_26

M3 - Paper

SP - 375

EP - 389

T2 - 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 1999

Y2 - 22 March 1999 through 28 March 1999

ER -

A theorem prover-based analysis tool for object-oriented databases

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this