Abstract interpretation for termination analysis in functional active databases

An active database consists of a traditional database supplemented by a set of Event-Condition-Action (ECA) rules. One of the key questions for active database designers is that of termination of the ECA rules. The behaviour of the ECA rules may be obscure and their semantics is often not specified formally. Consequently, developing termination analysis algorithms and prov ing their correctness is a challenging task. In this paper we address this problem for functional active databases by adopting an abstract interpretat ion approach. By "functional active databases" we mean active databases who se transaction execution semantics have been expressed in a purely function al language. Although we demonstrate our techniques for a specific active D BMS which supports a functional database programming language interface, th ese techniques are directly applicable to other active DBMSs whose executio n semantics have been specified using a functional or a denotational approa ch.