This thesis investigates the process of designing software from formal specifications, in particular, specifications expressed in the Z notation. The initial phases of software design have significant impact on software quality and the transition from formal specification to design is not clearly understood. There is often no visible or obvious connection between the specification and the finished design. It is possible to add traceability with either verification or refinement, but I wish to understand and guide the design process. Investigating the design of software from formal specifications highlighted possible relationships between parts of the specification and parts of the design. A design strategy is introduced, that combines software architectural styles and formal specifications to influence the generated design. The design process is architecturally-specific, but a template for instantiating the design process to a chosen architectural style is presented. Specializations of the template are presented for the ADT-based architectural style and the event-based architectural style. These specializations of the template produce an architecturally-constrained, specification-influenced design process. Providing an architecturally-constrained, specification-influenced design process enables the software designer to produce better quality software. The constrained design process allows the designer to focus on the difficult aspects of design: understanding the problem, choosing the best abstractions, and finding a suitable solution.
Identifer | oai:union.ndltd.org:ADTP/253804 |
Creators | MacDonald , Anthony John |
Source Sets | Australiasian Digital Theses Program |
Detected Language | English |
Page generated in 0.0022 seconds