Industrial Survey

The industrial survey was aimed to reach as many people as possible to get a wide range of opinion rather than that of a few recognised experts. The survey used a questionnaire which was designed so that it did not lead people to answer the questions in a particular way. The returned questionnaires were analysed with the help of software written in UNIX commands, in particular Bourne shell and `nawk' scripts.

The industrial survey attracted a lot of interest with over 400 questionnaires being returned. This survey is the largest of its type ever conducted in the area of formal methods with participants mainly from industry but with significant input from academics. It should be noted that the survey is mainly of the United Kingdom.

The survey has shown that the most widely used formal methods are VDM (55% - the percentage of the participants who voted with this response) and Z (55%). The formal methods which are used to specify concurrent systems e.g. , CCS and CSP (18%), are less widely used probably because they have been designed specifically for concurrent systems.

Formal methods are being integrated into the software life-cycle, most widely through structured methods (SSADM (15%) and Yourdon (10%) in particular) and much less through requirements analysis tools (like CORE (15%)).

Those who are using formal methods do so because customers require it (in particular the MOD and in security standards) or they work in the area of safety critical software which warrants best practice.

The survey shows three main reasons why formal methods are not being more widely used in industry:

• There is a lack of tools for formal methods, in particular commercially supported tools. There could be several reasons for this: not large enough market, lack of standards (of the most widely used formal methods only is standardised) or not clear what type of tools are needed. An obvious way to improve this would be to get VDM and Z standardised in such a form that effective tools can be built.

• It has not been shown conclusively that there are cost benefits to be gained from the use of formal methods in producing software.

• Many of the barriers (and limitations) to the use of formal methods are the symptoms of the process of change from the use of one technique to a completely different one. This process will take some time to work itself out.

Of the above three reasons the lack of tools was confirmed by the literature survey, but not the other two. The literature survey proposed instead that the use of mathematics was a problem but the survey of industry did not confirm this.

The survey has shown clearly that people are not aware of any good techniques for assessing objectively the contribution of formal methods to the quality of the software.