Formal representation and application of software design information

This dissertation describes the development of methods for formally representing and applying design information that enables user determined software design decisions to be automatically and correctly applied to software requirements producing a software design.; Formal methods for developing software use mathematical frameworks to specify, develop and verify software systems, especially safety critical systems where error free software is a necessity. A transformation system is a formal method that refines an abstract requirement specification into a concrete implementation by successively adding design decisions in the form of precisely verified design information. Current algebraic representations of design information (specifications, morphisms, and interpretations) and methods for applying algebraic specification design information (diagram refinement) cannot correctly represent and apply higher-level design information.; This investigation develops innovative methods for constructing and refining structured algebraic requirement specifications, as opposed to individual specifications. A category of diagrams and diagram morphisms is developed and applied to algebraic specifications and morphisms that enables the structure of requirement specifications and design information to be dealt with explicitly. Parameterized diagrams enable large requirement specifications to be built easier using a parameter passing analogy rather than with a diagram building analogy. Diagram interpretations enable structured design information to be correctly represented and applied, including the refinement of parameterized diagrams and restructuring refinements.; The developed approach enables one to create a library of correctly represented software design information. Software could then be developed directly from the requirements by selecting design choices from the library and correctly applying the underlying design information. Such a transformation system would enable correct-by-construction software to be developed rapidly and easily.