Next: 4 Protecting Against What
Up: Testing Formal Methods
Previous: 2 Introduction
Even the most dedicated formal methods zealot would admit that formal methods are a discipline where the divergence between ``academic'' and ``practitioner'' is enormous. On a day to day basis, my company deals with software organizations throughout the United States that develop the full spectrum of software applications: from operating systems and word processors to control software (avionics, air-traffic, embedded medical device, etc.) to games. And if there is one reoccurring theme throughout these organizations, it is that formal methods will never catch on until formal methods lesson the time-to-market and cost the same as the techniques they replace. After all, there is an awful lot of good quality software in use today that got hacked together overnight without formal methods. And as long as industry can operate in this mode, they will.
The argument that bugs caught earlier cost less over the life-time of a product does not outweigh a different concern: ``correct software that costs 100 times as much to develop and that misses the market window.'' And rightly so. The software industry moves fast. Time to market and costs are all that matters. The first ``usable'' product to market captures 100% of its marketshare. Recognize that even if a competitor of Microsoft were to come along with a bug-free document-editing package, they have no chance of stealing the market held by Microsoft Word.
If formal methodists (researchers) truly want the ``fruits of their labor'' used in the mainstream, they need to: (1) understand that generally speaking, marketing concerns outweigh quality concerns to development organizations, and (2) find ways to lessen the costs of employing them. If (2) cannot be successfully addressed, formal methodists will find their techniques only used in regulated industries.
Jeffrey M. Voas