OO-Method: An OO software production environment combining conventional and formal methods

Abstract

OO-Method is an OO Methodology that blends the use of formal specification systems with conventional OO methodologies based on practice. In contrast to other approaches in this field ([Jun95, Esd93]), a set of graphical models provided by the methodology allows analysts to introduce the relevant system information to obtain the conceptual model through a requirements collection phase, so that an OO formal specification in Oasis ([Pas92, Pas95-1]), can be generated at any time. This formal specification acts as a high-level system repository. Furthermore, a software prototype which is functionally equivalent to the Oasis specification is also generated in an automated way. This is achieved by defining an execution model which gives the pattern for obtaining a concrete implementation in a declarative or an imperative software development environment (depending on the user choice). The methodology is supported by a CASE workbench.