Jim Woodcock
Oxford University
I would like to emphasise five areas which I consider important: integration, case studies, education, tools, and addressing industry's needs.
For example, my work over the last fifteen years has often involved either Z or CSP, and the combination of these two methods is very appealing. On the one hand, Z describes states and operations very well, and on the other hand CSP describes concurrency and communication very well. Given that Z and CSP deal with complementary concerns, they could have been made for each other, and indeed there is much work which has been done in combining them. However, it seems to me that there are two considerations which are important when combining methods:
To fail to attend to the theroetical foundations of the combination is to miss out on the true advantages of formality. In chemistry, a distinction is drawn between an admixture and a compound. In an admixture, the ingredients merely mingle together; in a compound, the ingredients become chemically united. So it is with combining different formal methods. If the meaning of the combination is not properly explained, then the result is merely an admixture: nothing more can be deduced from the joint description than from the separate ones. If the meaning of the combination is explained, then the result is a compound formal method. It then becomes possible to have two views of a system specification, and to reason with and refine one view, and to understand the consequences in the other view.
For example, the collaboration in the 1980s between Oxford University and IBM Hursley Laboratories on the formalisation of the CICS transaction processing system focussed upon the use of mathematics to describe real software behaviour. The success of this work is well known, and resulted in the Queen's Award for Technological Achievement. Perhaps less well known was the work investigating the relationship between specifications and designs. As part of this, a designer described what was to him a valid refinement, but one which couldn't be verified by the existing proof rules for refinement. This was the point of departure for a research programme which lead to the discovery of a complete theory of data refinement, with its upwards and downwards simulations, and later to the single complete rule for data refinement.
In this way, the case study technique provides the experimental science which provides the problems for which theory must account. It also allows conclusions to be drawn about the suitability of each method on very large-scale systems.
For example, I was involved with an ex-student in the development of sooftware to manage an elaborate data structure within a new product. Like many industrial applications, this one is commercially confidential. However, let me say that it was for a large computer company, and involved a novel product. The development team were having difficulties in developing the algorithms for the data structure, so we started from the specification and calculated a design, and, eventually, the algorithms. We set out without knowing what the algorithms were, we followed the methods that we have developed, and we discovered the algorithms. This is a demonstration that increases confidence in the industrial strength and suitability of the techniques (Z + action systems).
Not every attempt at an industrial case study is immediately successful, however. I was engaged over a long period of time as a reviewer of a large project which was building a secure computer system for the British government. Although this project was, by its very nature, secret, it is now de-classified, and Rodger Collinson of CESG (a British government security establishment) published a paper on it at the Formal Methods Europe Symposium in Barcelona in 1994. The project developed Balzac, a theorem prover for Z, and a theory in Z of secure, state-based systems. Specification were written in Z of the various system components, and completely formal, mechanised proofs were then attempted to show that the system being built was indeed secure.
Unfortunately, the project became very bogged down in the details of its proofs, and the work was eventually scrapped. In the commercial sense the project was therefore a failure, since it did not produce the secure system that was intended. But the experiment was not unsuccessful scientifically, as we were able to draw three conclusions:
Addressing the problem of characterising and proving security properties has led to an immensely promising research programme in computer security using CSP and its model-checker, FDR. The result is a well-developed and intellectually-satisfying theory of security in CSP, where formal proof is replaced by automatic checking. Amongst its recent successes is the breaking of the Needham-Schröder authentication protocol.
Addressing the problem of mechanising Z has also led to interesting research in the semantics and logic of Z which have proved valuable in its BSI Standard. It has also led to a programme of research in mechanical theorem proving and tactic languages.
So, the point is that case studies reveal important insights into the application of our methods to real problems, and into the problems themselves.
http://www.comlab.ox.ac.uk/igdp/
I believe that we should automate whatever is useful: model checking, theorem proving, animation, testing. However, I would also stress that there have been many applications of formal methods that have used no tools whatsoever, and so we should not forget that the use of a formal method as an intellectual tool is very strong indeed. For example, the IBM CICS work was done largely without tools of any kind. There is a trade-off to be made between the added confidence obtained by machine-checking specifications and developments and the costs of obtaining that added confidence. I doubt very much whether the IBM CICS work would have been enhanced by the availability at the time of a theorem prover.
In another confidential project, I worked as a consultant during the development of an interesting new banking device. The project had many strands in it, developing new hardware and software. I was involved in the verification of the security protocol for moving electronic money around. We had to convince an independent evaluator that the protocol would not permit users to manufacture money. It was a fascinating piece of work, and involved some new theory in refinement; it did not involve any tools, except a parser for the Z specifications. Eventually, we satisfied ourselves about the system, did the proofs, and obtained the necessary certificate of security. The only part of the project which was brought in within budget and on time was ours--the formal methods part. The more traditional engineering parts were not so fortunate. The lesson I would draw from this is that the level of tool support was exactly right: any more woould have sunk the boat.