An Engineering Approach to Atomic Transaction Verification: Use of a Simple Object Model to Achieve Semantics-based Reasoning at Compile-time

D. Spelt, S.J. Even

Research output: Working paper

16 Downloads (Pure)

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.
Original languageEnglish
Number of pages16
Publication statusPublished - Sep 1998

Keywords

  • EWI-5984
  • METIS-118664
  • IR-18145

Fingerprint

Dive into the research topics of 'An Engineering Approach to Atomic Transaction Verification: Use of a Simple Object Model to Achieve Semantics-based Reasoning at Compile-time'. Together they form a unique fingerprint.

Cite this