Skip to main content
eScholarship
Open Access Publications from the University of California

Specification, verification, and enforcement of semantic integrity using behavioral abstraction

  • Author(s): Leveson, Nancy G.
  • Wasserman, Anthony I.
  • et al.
Abstract

This paper presents a method for the specification, verification, and enforcement of semantic integrity using behavioral abstraction. The specification contains both the abstract invariant of the abstract object (the static characteristics of the data) and the legal operations on the objects as defined by pre and post conditions (the behavioral characteristics) which preserve this invariant. The integrity specifications can be verified by proving that the abstract operations preserve this invariant. A practical means for enforcing integrity leads naturally from this integrity specification technique.

Main Content
Current View