Jonathan Lee, Jiann-I Pan and Wei T. Huang
Software Engineering Lab.
Department of Computer Science and Information Engineering
National Central University
In this paper, we propose an integration of an extension of Bailin's object-oriented requirements specification (OOS) with a formal notation (Z), called OOSZ. In OOSZ, the extended OOS is used to guide the derivation of Z specifications. A function process is converted into an operation schema. An entity process is manifested through a state schema, an instance creation operation schema and an abstract operation schema in the Z specifications. These are illustrated using the problem domain of Auto Banking Systems. The bringing together of diagrammatical and text elements of OOS specifications in Z notations offers three major benefits. First, OOSZ provides a systematic approach to producing a requirements specification which is both structuredand formal. Second, the OOS can be used to aid the analyst's understanding of the system for developing the Z specifications. Third, the OOS specification is improved by the precision of Z and through insights into the system gained during formalization.
Keywords: software engineering, requirements specification, methods integration, Z specifications
Received May 17, 1996; revised August 16, 1997.
Communicated by Y. S. Kuo.
*This research is supported by National Science Council (Taiwan, R.O.C.) grant NSC85-2213-E-008-005.