On the systematic transformation of requirements to specifications

Formal approaches to development are widely acknowledged to have difficulty in the validation of real-world requirements; in contrast, non-formal approaches find it difficult to identify the formal structures in requirements that are useful in a solution. That the problems that computing treats are embedded in the real world with solutions being an essentially formal machine means this dichotomy will always exist, with some new approach to the development needed which can draw a boundary between what is formalised and what can be left informal. In this paper, we show how the natural cause-and-effect structures that can be found in non-formal requirements descriptions can be used systematically to arrive at a software specification. The theoretical contribution of the work is the formalisation of Jackson's idea of problem progression in his Problem Frames framework through the use of a graph grammar to capture problem models as graphs and their manipulation as transformations. The approach is illustrated through a substantial benchmark example-Swartout's and Balzer's package router. We also report on the results of an initial empirical evaluation of the approach based on a prototype problem progression tool we have constructed.