OO and Active Formal Information System Specification

Abstract

Formal methods for Information System Specification is a field with a wide work background. Using an Object-Oriented model with a well-defined logical framework it is possible to execute the specifications as deductions in the formal first order theory equivalent to each specification, as was shown by Ramos [2]. The system implemented there is a powerful tool for rapid prototyping and constitutes a useful environment for open and passive IS that we call MOL (Micro-ObjectLogic). Using ideas for graphical object oriented design from [4], a wide spectrum OO specification language is presented in Bearing et al.[S] dealing with Open and Active Specification of IS (OASIS). The present paper is a first working version of this enhanced OASIS, built by adding to MOL active capabilities for expressing active relationships between objects by means of the triggering relationships. By active we mean that the objects involved are necessary for changes of state to take place, which is done by defining triggering conditions.

We then present what we mean by OO model. The third section states our class definition. The fourth presents the provided interaction mechanisms between objects and finally we present the prototype as it has been implemented, giving the syntactic language constructions and commenting on the most relevant implementation features.