The five papers above represent five different views from five researchers with different backgrounds. But it is interesting to note several points of convergence.
Almost unanimous is the view that formal techniques still must prove themselves. They have not yet been successfully integrated in the telecommunications software engineering process, and are still facing a 'documentation' and 'training' problem. Much of this may be a consequence of the different aims of the two communities involved: the people who developed the FDTs were mainly professional researchers, interested in proving an idea and then going to the next one. Industry penetration however requires a lengthy effort of technology transfer and development. This difference of intents appears obvious when one reads the papers of conferences such as ours: university papers tend to be heavy on novelty and formalism, with very simple examples. Industry papers report on industrial-size use cases, but the techniques are straightforward. Further, industrial papers tend to insist on lifecycle aspects, which are usually ignored by academics (Dembinski, Rudin).
A related problem is the one of 'reverse engineering' of legacy code into a form where formal techniques can be used. This problem is constantly mentioned by industry people. Its importance is due to the fact that today much of the software development effort is based on existing code which is continuously restructured and modified. Formal techniques must find their place in this process. Little research exists in this area.
The general-purpose formal methods prevalent until recently (based on the use of general-purpose specification languages and verification tools) are yielding to special-purpose methods, which use domain-specific properties. In the protocol verification domain, 'model checking' is cited by several panelists as the most successful and promising method. This tendency towards special-purpose methods and finer-grade customization will increase, because the more application-specific the methods become, the more information can be used to speed up the specification and verification process, and the more easily the results can be interpreted by the engineer (Zave, Courtiat). For example, there will be systems designed to verify the functionality of specific types of PBXs or LANs. Such systems may be similar to systems in industrial use today for this purpose, but may also use advanced concepts based on software verification theory.
When several types of application-specific methods are used, each will bring with itself its own formalisms, hence the need of attention to the question of formalism integration (Courtiat, Holzmann and Zave). In this respect, one can only regret the fact that the theory and application of each existing FDT is being developed in isolation, with little attention to mutual integration.
There appears to be a consensus that there is a bright future for formal techniques, although achieving this will require considerable additional work.