The Queen's Award for Technological Achievement 1992

This award was made jointly to OUCL and IBM, for their collaboration in the use of formal methods -- "notations, theories, and processes", and specifically the use of the Z notation -- in the production of transaction processing software -- and specifically the Customer Information Control System (CICS) products in IBM's Enterprise Systems Architecture (ESA) environment.

For a decade, Oxford University Computing Laboratory and IBM UK Laboratories, Hursley Park, had been collaborating closely on the development of modern software engineering techniques, and their use in industrial practice. OUCL had been offering advice on mathematical techniques relevant to IBM's work, and helping IBM to apply them.

Central to this collaboration has been the use of Z: in essence elementary set theory and logic, engineered into a notation suitable for the specification, development and documentation of software systems; together with techniques and styles of use. The aim of applying this "ruggedised" mathematics to the development of computer programs is to reduce the costs and risks of the process of development, and to improve the quality of the product -- which itself reduces the costs of subsequent maintenance.

Before the collaboration which this award recognises, the use of Z had been confined mainly to small exercises, and largely within Oxford. The collaboration began tentatively, with small experiments to see whether Z really could be used in an industrial environment. Case studies which came from these experiments have proved useful foundations for subsequent work, but the most useful outcome was a significant transfer of culture -- in both directions -- between the academics and the practitioners.

It was then decided to use Z to develop the next release of a transaction processing system, CICS/ESA_V3.1, and to this end Z was integrated into IBM's existing and well-established development process. This demonstrated that it was possible to manage a large and important software development using mathematics.

Many measurements of the process of developing CICS/ESA_V3.1 were conducted by IBM, and they estimated that over all the other benefits of the experiment they were able to reduce their costs for the development by almost five and a half million dollars. Early results from customers indicate significantly fewer problems, and those that have been detected are less severe than would be expected otherwise.

The mingling of cultures has been of substantial benefit both to Oxford and to IBM. A choice example is the resolution of a problem in describing the correctness of a data-refinement step. One of the CICS designers knew that the step was valid, but the theory of refinements was unable formally to justify it. Research into this problem gave rise both to a new theory (complete in the technical sense), and a (complete in the usual sense) formal justification of the actual refinement.

The industry in general has benefited from IBM's support and encouragement for the standardisation of Z. The syntax and semantics in the standard are both closely based on work funded by IBM. Throughout the project there has been a policy of open publication, both of techniques and results, to an extent which has been unusual for IBM in projects of this kind. This openness has contributed not a little to the acceptance of formal methods in other parts of the industry (and in particular to the spread of Z).

It is pleasing to be able to acknowledge that IBM's contribution to this work included not only their own staff's time and financial support of staff at the laboratory, but also the bravery to commit to an experiment involving a substantial product development, and the persistence to see it through. There has been a good understanding at all levels of management in IBM of what formal methods can and cannot do: this has enabled them to direct the Laboratory's research at the most pressing problems.

Education has been an important part in this work: OUCL has taught these methods both to the students on its MSc in Computation course, and on external courses to commercial organisations, including of course IBM. (Courses in Z and its use are now also given by other organisations.) IBM has developed its own courses in consultation with Oxford, and this transfer of technology is as much a benefit of the collaboration as are the others, and is a welcome indicator that IBM had accepted that it had a stake in the methods. Students from IBM have been amongst the first to undertake the part-time Postgraduate Diploma and MSc in Software Engineering.

Selected bibliography

This work has been well-documented in the scientific literature, and there is a substantial and flourishing bibliography. These are a few of the documents relevant to this project:

S M Brien,

Z Base Standard - Version 0.5,
Oxford University Computing Laboratory, ZIP/PRG/91/43, 1991.

B P Collins, J E Nicholls, I H Sørensen,

Introducing Formal Methods: the CICS Experience with Z,
Technical Report TR12.260, IBM Hursley Park, December 1987.

B P Collins, C J Nix,

The use of software engineering, including the Z notation, in the development of CICS,
Quality Assurance. 14(2):103-110, September 1988.

P H B Gardiner, P J Lupton, J C P Woodcock,

A simpler semantics for Z,
in Z User Workshop, Oxford 1990, Springer Workshops in Computing, 1991.

I J Hayes (ed.),

Specification Case Studies,
Prentice Hall, 1987.

P Johnson,

Experience of formal development in CICS,
in J McDermid (ed) The Theory and Practice of Refinement, Butterworths, 1989.

S King,

Z and the Refinement Calculus,
PRG Technical Monograph PRG-79, Oxford University Computing Laboratory, 1990.

S King,

The use of Z at IBM Hursley: experience and results,
Oxford University Computing Laboratory, 1991.

S King, I H Sørensen, J C P Woodcock,

Z: grammar and abstract and concrete syntaxes,
PRG Technical Monograph PRG-68, Oxford University Computing Laboratory, 1987.

P J Lupton,

Promoting forward simulation,
Z User Workshop, Oxford 1990, Springer Workshops in Computing, 1991.

M A McMorran, J E Nicholls,

Z User Manual,
Technical Report TR12.274, IBM Hursley Park.

J C P Woodcock,

Mathematics as a management tool: proof rules for promotion,
in B A Kitchenham (ed) Software Engineering for large software systems, Elsevier, 1990.

J C P Woodcock,

Calculating properties of Z specifications,
ACM Software Engineering Notes, 14(5):43-54, 1989.

J B Wordsworth,

Formal methods in the development of CICS,
BCS Computer Bulletin, December 1987.

J B Wordsworth,

Program construction from a formal specification,
The Theory and Practice of Refinement, Butterworths, 1989.