engineering approach to atomic transaction verification: use of a simple object model to achieve semantics-based reasoning at compile-time

Share/Save/Bookmark

Spelt, David and Even, Susan (1998) engineering approach to atomic transaction verification: use of a simple object model to achieve semantics-based reasoning at compile-time. [Report]

[img]
Preview
PDF
411Kb
Abstract:In this paper, we take an engineering approach to atomic transaction verification. We discuss the design and implementation of a verification tool that can reason about the semantics of atomic database operations. To bridge the gap between language design and automated reasoning, we make use of a simple model of objects that imitates the type-tagged memory structure of an implementation. This simple model is sufficient to describe the operational semantics of the typical features of an object-oriented database programming language, such as bounded iteration, heterogeneity, object creation, and nil values. The same model lends itself to automated reasoning with a theorem prover system. We are thus able to apply theorem prover technology to verification problems that address transaction semantics. The work has applications in the areas of transaction safety, semantics-based concurrency control, and cooperative work. The approach is illustrated by a graph editing example, with heterogeneous node structures.
Item Type:Report
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/18145
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 118664