Validating database constraints and updates using automated reasoning techniques

Remco Feenstra, Roelf J. Wieringa

    Research output: Contribution to conferencePaperpeer-review

    30 Downloads (Pure)


    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.
    Original languageUndefined
    Number of pages9
    Publication statusPublished - 1995
    EventWorkshop on Semantics in Databases - Prague, Czech Republic
    Duration: 1 Jan 19951 Jan 1995


    WorkshopWorkshop on Semantics in Databases
    OtherJanuary 1995


    • IR-76206
    • EWI-10654
    • SCS-Services

    Cite this