Using box structures with the Z notation

The Box Structure Method (BSM) of analysis and design provides a framework that can be used to introduce formality into the requirements specification stage of software development. A method of requirements specification is presented which integrates the Z notation with BSM. The requirements specification is confined to the top level black box specification and the corresponding top level state box specification. We describe criteria for good requirements specification and we explain advantages of our integrated method for achieving them. Summary introductions are given to both BSM and Z followed by an examination of the relationship between the two methods. We explain our integrated method and illustrate it using a simple birthday reminder system. This method has been used to give a mathematical model of a tool called the Box Structure Assistant (BSA). The Box Structure Assistant is a planned system to provide tools for managing, editing, and printing system designs using the C Design Language. The BSA black box and state box requirements specifications are presented in a case study. Finally, we discuss issues that have emerged from the use of this method and indicate areas for future research.