Formal characterizations for active database specification, verification and maintainability

In this thesis, we make several contributions towards developing a more formal approach for systematic design of active databases. We present a formal characterization of active databases by developing a specification language and defining the notion of correctness of an active database with respect to its specification. In the specification language, we distinguish between the notions of ‘invariance’ and ‘maintenance,’ and propose four different classes of specification constraints. We also propose three different types of triggers with distinct purposes, and show through the analysis of an example from the literature the correspondence between these trigger types and the specification classes. We then define the evolution of an active database in terms of states and transitions. We define when an evolution due to updates and triggers satisfies a given specification.; We use the smodels [59] declarative logic programming language to show how both the specification of active databases and the evolution due to updates and triggers can be encoded in smodels. We first show how temporal and aggregate constructs can be expressed in smodels. We then describe how various possible evolution paths of an active database due to different initial states, updates and triggers can be expressed using the ‘choice’ and ‘enumeration’ feature of smodels. Since the smodels language has an interpreter that can be executed, our encoding leads to a methodology to verify correctness of some aspects of active databases. We then consider a detailed active database example from the literature and illustrate our approach using this example. Finally, we extend the notion of maintenance constraints to a notion of maintainability in autonomous agents [68] and briefly mention its relevance to reactive databases where exogenous updates require an immediate response.