Validating database constraints and updates using automated reasoning techniques

In this paper, we propose a new approach to the validation of formal specifications of integrity constraints. The validation problem of fornmal specifications consists of assuring whether the formal specification corresponds with what the domain specialist intends. This is distinct from the verification problem, which is the problem whether an implementation (which is a formal object) corresponds with a specification (which is also a formal object). We consider formal specifications of object-oriented database systems that are subject to static and dynamic integrity constraints. To validate that such a specification expresses what we intend, we propose a system that can answer reachability queries, in which it is asked whether the system can evolve from one state into another without violating the integirty constraints. If the query is answered positively, the system should exhibit an example path between the two states; if the answer is negative, the system should explain why this is so. We discuss the use of planning and theorem-proving techniques to answer such queries, illustrating their application to reachability queries relevant for database system validation.