Background and Motivation

In 1985 I was invited by Roger Stokes to join the then recently formed Defence Technology Centre in ICL to work on the application of formal methods to the development of highly assured secure computer systems. I transferred to DTC at the beginning of 1986.

A couple of years later, when the group had grown to five people Roger Stokes, preferring to continue technical and consultative work rather than be drawn into administration and management, relinquished the lead to me, which position I have held ever since.

In those days we had little occasion to consider whether formal methods were worthwhile. Others, notably GCHQ, had decided that they wanted to undertake development of secure sytems to very high levels of assurance, were contracting the work to industry, and had laid down regulations and guidelines requiring the use of formal methods in such developments.

GCHQ spent many years stimulating the development in UK industry of a capability for developing secure systems using formal methods. To that end GCHQ initiated a program to develop components, or building blocks, from which secure networked systems might be built. These building blocks were intended to be built to what is now known as E6 assurance in the ITSEC secure systems evaluation guidelines.

However, we would like to sustain and rebuild our work in formal methods. More radical rethinking is necessary if we are to continue to exploit our skills and IPR in formal methods.

I have given (and continue to give) a great deal of thought to marketing strategy in the broadest sense of that term, in which it is essentially synonymous with "business stategy".

The first "strategy" was to use ProofPower, not originally intended as a commercial product, as a way of achieving greater visibility in the marketplace for ICL and reaching a more diverse customer base. In the former it had some success, but in the latter it had insufficient success. Most particularly we had hoped that there might be some business in the safety critical area arising from the requirements for formal methods in the development of defence related safety critical software established in the UK by Defence Standard 00-55. For a while this looked plausible, but for ICL no significant business ever arose. It is still a matter of uncertaintly to what extent critical systems will provide a future business for companies specialising in formal methods.