Verification of Compensation Requirements for the SEPIA Cooperative Authoring System
Susan Even, David Spelt · 1998
Compensation plays an important role in advanced transaction models, cooperative work, and workflow systems. However, in spite of the fact that the correctness of a system may depend on compensation operations, little attention has been devoted to the specification of these operations and the verification of their ability to compensate. In fact, compensation operations are often simply written as a -1 (ignoring any parameters or results) and are assumed to be provided by the implementor of a system. This unfortunate situation reveals a significant (and obvious) gap between theory and practice. In this paper, we introduce a framework for the formal analysis of compensation operations, using an automated theorem prover. This framework includes: a high-level object-oriented schema definition language, an automated mapping from this language to a model in higher-order logic, and theorem prover extensions for mechanically reasoning about the database operations. As an example, we ...