Evolving logical specification in information systems

Traditional logic-based specification approaches fix the structure and the dynamics of an object system at specification time. Information systems are applications with a very long life-time. Therefore, object and specification evolution to react on changing requirements is a relevant aspect of describing information systems as object societies. We present a logical specification framework for evolving objects based on the concepts of object developed for the languages Troll and Gnome and the underlying temporal logic OSL. The syntactic notion of object descriptions is extended to explicitly manipulate temporal axioms during behaviour evolution. An extension of OSL called dyOSL establishes a logical framework where basic temporal formulae are evaluated by a second logical layer. dyOSL explicitly manipulates state-dependent sets of temporal formulae to model evolution of object axioms. Syntax and semantics of dyOSL are given together with a translation of the specification language constructs into dyOSL. The corresponding proof theory is discussed together with guidelines for formally certifying object properties. Additionally, we show the use of the formalism for some specific information system scenarios. (orig.)Available from TIB Hannover: RR 4487(1997,5) / FIZ - Fachinformationszzentrum Karlsruhe / TIB - Technische InformationsbibliothekSIGLEDEGerman