The software crisis of the late seventies created an atmosphere of hope with respect to FMs which was impossible to satisfy mainly because of the hardware/software technology which was available at that time. This was one of the reasons why formal methods could not be applied to software of practical size and utility. The combination of hope and inability resulted in a widespread opinion among industry and practitioners that FMs were something that one had to tolerate (or even, officially, to support) but no one had the intention to use in his/her own practice. Unfortunately, popular opinions have long lives and are hard to change.
I firmly believe that the above popular opinion is unjust. It neglects the role of FMs in the past, their present considerable achievements, and future perspectives due in part to the enormous technological progress over the last few years.
A need for abstraction and formalization has existed in computer science since the very beginning. Therefore, FMs were born very early. In a schematic and simplified form they started from concentrating on the relationship between
Over the years, the level of abstraction and the topics of interest have changed. Sequential, mono-processor programming has evolved towards software for distributed, communicating systems, executed in multiprocessor or networking environments. The complexity of the present systems and of the problems to be solved enforced formalization of problem requirements which, earlier, were considered satisfactorily defined in informal, natural language terms. Therefore, today's FMs deal rather with problems relating to
Changing the level of abstraction should not suggest that one has to restart from the beginning, because just the opposite is true. Almost all present mathematical foundations of computer science, including verification theories and semantic concepts, have their seeds in experiences gathered (but sometimes unjustly forgotten) in the sixties and early seventies, while discussing and defining the syntax and semantics and compilers for so-called higher-level programming languages (for a compendium of this theoretical background see [4]).
If I claim that the popular image of FMs created 10-15 years ago is no longer valid, I am also thinking about the tremendous technological progress that made some earlier dreams possible. One such dream, with respect to software verification, could be worded as follows: if one had a computer extremely fast and extremely large (in terms of memory), one could automatically verify a given property in all possible situations generated by a given program (system). The model checking approach tries to realize this dream with growing success, exactly because of technological progress but also because of a solid theoretical base established earlier. This seemingly brutal and simplistic approach is very appealing because of its external simplicity but, in order to be effective (no matter how powerful computers are) it needs very sophisticated underlying methods (e.g., to reduce the search space) and requires new solutions of very interesting mathematical problems. Techniques related to model-checking are being developed rapidly and will be the first to be practically accepted.
There is a lot to be done in the near future. Requirement specification languages are often not expressive enough. In particular, they rarely treat problems of real-time and time constraints in general. Although formulae in temporal logic relate past, present and future events, they still do not express many interesting timing conditions. Also, a lot has to be done to make the requirement specification languages and their supporting tools user-friendly.
System-level specification formalisms are also far from perfect (time constraints!). Each of the FDTs has its strong points (graphical SDL representation may be an example) and has a lot of very elaborate tools based upon it. It is essential that specifications be verifiable with respect to requirements. FDTs all proved acceptable as inputs to model checking verification techniques. This is a good indication. But all of them have the same flaw: they are not (efficiently) executable. This seems to be a result of the confusing role that was assigned to them at the beginning: a role of languages that were meant to formalize standards independently of implementations, but also of languages that were to allow for some computational experiments with the standards specified. I strongly believe that, in order to be accepted and used, FDTs (and, more generally, system-level specification formalisms) have to be not only better designed, but also designed for automatic implementation, with "ordinary" programming languages playing the role assemblers had in the past. Without an effort in this direction it is possible that FDTs will remain confined to the academic realm.
In conclusion, I think that FMs have entered a very challenging period in which the efforts of the past have a real chance to be appreciated.