A STRUCTURED SPECIFICATION OF ALL ACTIVE DATABASE SYSTEM

Active database systems are a current focus of considerable research interest, as a means of supporting a range of tasks including constraint enforcement, real-time applications and derived data management. However, although many different proposals have been made-for active rule systems, such proposals are normally described in an informal manner, which makes it difficult to understand how different proposals differ or how a set of rules will behave. This paper compares a range of formal specification methods, considering how suitable they are for describing active database functionality, and then shows how the model-based notation Object-Z, an object-oriented extension of Z, can be used to specify the semantics of a representative active database system, namely Starburst.