For well over fifteen years, we have been predicting successful application of our formal methods to problems in the real world. Until two years ago, however, little success was evident. Since then, there has been an explosive growth in the sales and use of two commercially distributed SDL-based tools. While this growth is exciting, I fear that, in the future, we may find ourselves on a course that will prevent us from attaining the degree of success that might have been possible.
The bright stars on the horizon are the tools SDT and GEODE, developed and marketed by Telelogic in Sweden and Verilog in France, respectively. Based on SDL, (Specification and Description Language) these tools are packages for creating and editing protocol definitions, testing the definitions for self-consistency and consistency with sequences specified in MSC (Message Sequence Chart) language, compiling the specification into C and other implementation languages, and validating the protocol (using techniques published in this IFIP PSTV/FORTE conference series).
Together, Verilog and Telelogic have sold some 7500 licenses for these tools. It is exciting to note that users and institutions are willing to spend several thousand dollars to acquire such a license!
Of the best-known FDT languages, SDL probably comes closest to allowing a designer to express himself using relatively conventional design techniques. This of course has contributed significantly to the success of these tools. Moreover, the commitments of Verilog and Telelogic to the user, in terms of providing attractive, easy-to-use, and time-saving graphical user interfaces, boosted sales of both development systems. One is obliged to conclude that satisfying user needs --- providing functions users need in a user-friendly fashion in a language users like --- is a key to success.
There is a real schism within our research community between theorists and practitioners. Many of our papers begin with a common rationale concerning the benefits of formal methods: a lack of ambiguity in specification and a basis for the use of powerful analytic tools to verify properties, and to implement and test real protocols. The implication is that a given author intends for his or her work to be used for real-world protocols. In reality, the majority of authors leave the application to real-world protocols as the proverbial "exercise for the reader"!
Only a few authors have attacked real protocols. In my view, these few have been successful in applying techniques that are already available. This is not a cookbook task: most real-world protocols are complex and it takes considerable effort to understand them. And, whereas several techniques are known, it does take considerable ingenuity, creativity, and skill to apply them to real protocols.
I believe this gap between claimed and actual capabilities has cost us dearly in terms of credibility: If these claimed capabilities were half as powerful as we claim in our prefaces, where is the long list of successes?
There is a real need to apply formal methods in the world of communicating systems design. Success can be ours, but I believe there are three requirements for achieving this success:
Until our research community aims at solving our customers' (users') problems, we will suffer the fate we deserve! More of our work should
In conclusion, the time is ripe for a change in our strategy. We should carefully consider how the fruits of our research fit into the user's complete design process of specification, validation, implementation, testing and maintenance.