next up
Next: About this document Up: Workshop position paper on

Workshop position paper on strategic research directions in formal methods

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.

  1. Integration I believe this to be one of the most important research areas in the field of formal methods, and it falls into two parts.

    1. Integration of methods The term ``formal methods'' is actually rather misleading, since it is usually used as a classification of things which are not ``methods'' at all, and certainly not methods where the sequences of actions undertaken is formally defined. Rather the term has come to be used for the class of formal systems which have been created specifically to be useful for the development of complex systems, together with the associated guidelines for the formal system's use on real problems. No one formal system is ever likely to be suitable for describing and analysing every aspect of a complex system, so a ``formal method'' is not the method which a system designer might choose to use when developing a system, but one of the tools that a designer might wish to make use of during the process.

      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:

      1. finding a suitable style for using different methods together; and
      2. finding a suitable meaning for using different methods together.
      Very often neither is addressed adequately. To fail to find a suitable style is to miss out on the true advantages of combining methods. For example, the Z school have always stressed the importance of presentation of specifications in an accessible form, with plenty of natural language. This has surely led to the notation's popularity. Any combination must preserve this style of presentation.

      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.

    2. Integration with current practice I believe that we must understand better how to use formal methods in a practical way. A key part of this is to integrate their use with other software engineering techniques. In particular, I believe that it is vital to exploit the relationship with testing techniques.

  2. Case study work The case study is an important research tool. It is essential for addressing the scaling problem, and for giving effective demonstrations. It can also be the source of good research problems.

    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:

    1. that Z is (in this case) appropriate for modelling the functional behaviour of a very large system;
    2. that Z is inappropriate for modelling security properties; and
    3. that Z is unsuited to large-scale mechanical theorem proving.
    The first point reinforced other experiences that indicate the industrial usefulness of Z (for example, the IBM CICS work). However, the second point came as something of a surprise: why shouldn't Z be just as useful in describing a non-functional property such as security? The final point was also dismaying: if Z is so good for understanding a system's behaviour, then why isn't it good for reasoning about it?

    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.

  3. Education I believe that education is vital to the success of the formal methods programme. At Oxford University, we have always taken technology transfer very seriously, and we teach our techniques to those in industry. I believe that the question of how to teach formal methods effectively is intimately bound up with the question of how to use formal methods effectively. I believe that we have gone some way towards this in our part-time MSc in Software Engineering, details of which may be found at
    http://www.comlab.ox.ac.uk/igdp/
  4. Tools Tools are very important to the success of formal methods. For example, CSP is very much more successful now that there is a toolkit to support it. The FDR model-checker has made it possible for CSP to move out of the classroom and into industry. Although it is not essential in industrial-scale application, it certainly helps when a formal method is used for anything more than modelling work. For this reason, if verified refinement steps were required, then I would recommend the B method over Z, for the simple reason that the former is highly automated, whereas the latter is not.

    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.

  5. Industry's needs I believe that formal methods is about using mathematics to develop real, industrial-scale programs. In looking to see what should be the strategic research goals for formal methods, I believe that we should look to industry's needs and see if we are fulfilling them. So what are these needs? They stem from the fact that commercial pressure to produce higher-quality software is always increasing. Success for industry depends upon
    • timely delivery
    • continuously-enhanced functionality
    • understanding customers' needs
    • re-use of legacy code
    • commitment to quality
    • elimination of errors
    • cost-effective development
    • real-time performance
    All of these present a considerable challenge to researchers in formal methods.




next up
Next: About this document Up: Workshop position paper on

TOM Comversion
Fri Jul 12 15:08:37 EDT 1996