An Ounce of Prevention is Worth a Pound of Cure: Formal Verification for Consistent Database Evolution

摘要

Consistency of a database is an important property that must be preserved at all times. In most OODB systems today, application code can directly access and alter both the data as well as the structure of the database. As a consequence application code can potentially violate the integrity of the database, in terms of the invariants of the data model, the user-specified application constraints, and even the referential integrity of the objects themselves. A common form of consistency management in most databases today is to encode constraints at the system level (e.g., foreign keys), or at the trigger based level (e.g., user constraints) and to perform transaction rollback on discovery of any violation of these constraints. However, for programs that alter the structure as well as the objects in a database, such as an extensible schema evolution program, roll-backs are expensive and add to the already astronomical cost of doing schema evolution. In this paper, pre-execution formal verification of schema evolution programs is proposed as an alternative solution to the traditional rollback solution for consistency management. As part of this work we introduce the notion of contracts, i.e., pre- and post-conditions for an extensible schema evolution program, and demonstrate that they can be specified using a familiar language, OQL. We also demonstrate the ease and practicality of using a theorem prover for the formal verification of schema evolution programs. The theorem prover tool can be set up initially with all the information about the environment, i.e., the axioms of the database, the invariants and the basic schema evolution primitives. A writer then of an extensible schema evolution program need only supply the contracts and the program written in OQL to guarantee the correctness of their program. We highlight the main features of the verification process using a complete walk-through example. The end result of our approach is a more efficient consistency management framework that has limited overhead to the users and yet provides flexibility to safely add new schema evolution transformations to the system while assuming complete correctness.