Doctoral Dissertations

Hailong Mao

Date of Award

12-1993

Degree Type

Dissertation

Degree Name

Doctor of Philosophy

Major

Computer Science

Major Professor

J. H. Poore

Committee Members

Michael Thomason, Michael Vose, Carl Wagner, Richard Linger

Abstract

The Box Structure Method (BSM) is a process of stepwise refinement and verification that derives a system design from a specification. The final product of the BSM is a usage hierarchy of data abstractions in which each abstraction is defined in three distinct forms: black box, state box, and clear box [1, 2, 3]. This dissertation recasts and extends BSM into a formal method of syntax, semantics, principles and methods called the Box structure Development Method (BDM). The goals of BDM are to enhance the rigor of software specification, design and verification in box structures and to make the process more tractable, predictable and repeatable. BDM provides formal definitions of well-formed types, black boxes, state boxes, clear boxes, and systems. Mills' original mathematical model for box structures is extended such that (1) the domain and range of a box are defined as the Cartesian products of domains of data types, (2) a well-formed domain predicate is added to the black box and state box to allow definition of partial functions on the "virtual domain," and (3) a well-formed mapping predicate is defined as a characteristic function for the black box and state box functions. Equivalence relations among stimulus histories, a theory of canonical stimulus histories, the relationship between canonical histories and states, and other mathematical properties holding among the black box, state box and clear box have been defined and studied. As a result, theorems have been established to provide insights and procedures for stepwise box structure expansion in routine software engineering practice. BDM contains a structured specification method for the specification of complex systems. The method provides for a stimulus history-based description, a canonical history-based description, domain partitioning and a specification hierarchy of black boxes. Theorems are provided to support systematic verification of completeness and consistency for such structured specifications. The four fundamental principles of the Box Structure Method, i.e., referential transparency, transaction closure, state migration and common services are treated formally. Transaction closure is subsumed in completeness and consistency. Referential transparency is treated as the substitutability of equals for equals. State migration is tied to a discipline of user interfaces and data accessibility. Finally, the principle of common services is formalized for both function and data abstractions.

Download
Files over 3MB may be slow to open. For best results, right-click and select "save as..."

Share

COinS