Formal Representation and Application of Software Design Information

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 a requirement specification into an 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 design information involving 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. 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 requirements by selecting design choices from a library. Such a transformation system would enable correct-by-construction software to be developed rapidly and easily