During 1986-95 I was employed be "International Computers Limited" (now absorbed into Fujitsu services UK) on the application of Formal Methods to the development of secure computer systems of various kinds, and on the development of the methods and tools to support such applications. The "Formal Methods Team" which I joined in 1986 and lead from about 1988 to 1995 was principally oriented towards participating in research and development contracts funded by CESG (part of GCHQ) intended to make the UK capable of developing computer systems sufficiently secure to be trusted with sensitive data coming to us from the USA. The USA had then in place standards for the development of secure computer systems which involved the use of formal methods on the supposition that the best way to ensure that these systems were indeed secure was through a formal mathematical proof.

When I arrived on the scene this programme of research CESG had been thus engaged for some time, and, had decided on the basis of advice from formal methods consultants that the work they were funding should be undertaken using the Z specification language.

Most of the work we did during this period was breaking new ground, certainly for us, and often (not necessarily in spectacular ways) seemingly for the field. Consequently, was is said under other headings (e.g. security, proof support, Z, VDM, HOL) often contains significant methodological content. Rather than try strip out or reproduce all the methodological content from these different topics, I propose to present here only the themes which apply fairly generally, and to mention very briefly and refer elsewhere to the methodological material which appears under the other headings.