Validating database constraints and updates using automated reasoning techniques


Feenstra, Remco and Wieringa, Roel (1995) Validating database constraints and updates using automated reasoning techniques. In: Workshop on Semantics in Databases, January 1995, Prague, Czech Republic.

Abstract: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.
Item Type:Conference or Workshop Item
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page