Background and Motivation

beginnings
making a business
bad news
rethinking

How I got into Formal Methods

I have been interested in logic for most of my life, since as long as I can remember actually knowing anything about it (since at least 1967).

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.

Turning it into a Business

For most of this time the formal methods team at ICL was not required to be managed as a profit centre. Revenue earning contracts from GCHQ provided the justification for increases in the team strength, but noone was counting whether we made a profit, and we were allowed to undertake part funded or unfunded work.

Withdrawal of The Customer

CESG wasn't our only customer, but did account for most of our revenue. This is a risky situation for any small business (which were eventually treated as), and the worst has happened. GCHQ has now completely withdrawn from sponsoring the development of E6 level secure systems, and its plans for further significant investment in tooling have been shelved.

We continue to benefit from formal methods related contracts with the UK Defence Research Agency, and from modest sales of ProofPower, but now we also have to turn our hands to security consultancy at levels of assurance which require no formal treatment.

Rethinking the Marketing Strategy

It has come to seem doubtful that the high assurance sector will provide a marketplace within which our team can sustain a profitable business. One direction of diversification, bringing the team more in line with its context in ICL, is to broaden the security skills and take on appropriate work in less highly assured developments. This line has been adopted and is proving succesful.

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.


. created: 14/4/95, modified 26/10/95.