A personal view of Formal Methods
Brian A. Wichmann · 2000
The original introduction of Interim Defence Standard 00-55 [13] created a controversy concerning the industrial application of Formal Methods which does not seem to have been resolved. Here, I am not concerned with the specifics of 00-55, but with the application of ‘Formal Methods’ in critical systems. The IEE and BCS have a common working group on the issue of Formal Methods with the aim of attempting to obtain a better consensus. Without such a consensus, discussions on the issue seem to be inconclusive and lack focus. The starting point for the IEE/BCS working party was an IEE brief [8], which was felt by BCS to be inadequate. Rather than make such a negative comment, the desire was to produce something which would be more incisive — but this has not yet happened, although a serious attempt has been made. This paper is a personal contribution to the debate which I hope will eventually allow the Institutions to produce effective guidance on this topic, that is when and to what extent, ‘Formal Methods’ should be used. This paper is concerned with using methods like VDM-SL and Z to specify discrete systems of a general nature. More specialized methods which are formal but have a smaller range of application have often been more successful in their application. For instance, the use of SDL in the specification of network protocols has resulted in techniques for the automatic generation of test cases which has been very successful in the quality assurance of network software. These more specialised applications are not considered here. If I am asked for a single phrase to encapsulate my views on Formal Methods, I would quote John McDermid’s remark: ‘Oversold and under-used’ [14]. Unfortunately, this remark merely highlights the dilemma: how can formal methods be sold more effectively so they are not under-used? In this paper, I consider this problem almost entirely from the point of view of producing safety systems involving software. I do not have personal experience in other high integrity areas, such a security, although I suspect the situation is similar. As part of the IEE/BCS working group activities, a workshop was arranged at IEE with participation by invitation. The attendance was good, the discussion lively, but I did not feel that the resulting write-up [21] did result in the advice which I think