Note: this page is no longer maintained.
The attitude that formal methods is too expensive to use stems from the narrow interpretation of formal methods as a complete application of code-level verification. When viewed as a more flexible analysis technique, usable at different points in the life cycle and with varying degrees of coverage, the cost issue ceases to be forebidding. Experience with trusted system development efforts yielded costs in the range of 10-20% for "A1" systems. The NIST survey of applications by Craigen, Gerhart, and Ralston likewise indicates a range of positive findings. While everyone would like to have better cost data, the evidence we have so far does not support the feared unaffordability of formal methods. Moreover, as progress is made and we develop a sizable body of reusable "deductive assets," costs will drop considerably.
The attitude that formal methods does not scale also stems from the interpretation of formal methods as merely code-level verification. The types of real systems to which formal methods have been applied, in one form or another, include: operating systems, networks and their supporting software, real-time embedded controllers, microprocessors and other hardware subsystems, and special-purpose security devices. Many of these applications are chronicled in the NIST survey. Pilot projects for aerospace applications now underway include requirements analysis for the Space Shuttle and other space programs as well as critical subsystems for commercial aviation. What is clear from these enterprises is that by taking an open-minded and adaptable approach to formal methods, many real problems can benefit from the increased modeling and analysis capabilities.
In addition to addressing these two false impressions of formal methods, I would also like to address one or more of the following issues:
Formal methods is not an all-or-nothing matter. Formal techniques can be used for stating requirements, analyzing requirements, specifying code, analyzing the conformance of source code to specs, analyzing translation of source to object, analyzing the hardware on which the object code runs, etc. Any of these can be worthwhile even in the absence of the others. Our own experience is that writing formal specifications is an effective way of finding immediate problems and forestalling long-term problems with maintenance, etc. We believe that we are more successful at finding coding errors by walking through implementations with the formal specifications in hand.
Finally, a large and useful subset of Ada can be specified and reasoned about formally. The most complex parts of Ada are static semantics, tasking, and optimization (section 11.6). We can claim to have proved that the canonical dynamic semantics (i.e., no 11.6) of sequential Ada is clean -- namely, by producing a sophisticated, but relatively short, semantic definition that can actually be used to reason about programs. Furthermore, such complexities as are introduced by 11.6 are not intrinsic to Ada -- they're present, and swept under the rug, in all its obvious competitors.
Mathematical modeling guarantees perfection.
As engineers we use mathematical techniques to provide increased assurance, not absolute assurance. Logic is just another branch of mathematics that can be applied in a variety of ways to the development of both software and hardware systems. It enhances our ability to predict the behavior of systems before they are fielded. But ultimately these systems have to face the real world for which our mathematics is only an approximation.
The claims that formal methods is a straight jacket and that formal methods is simply code-level proofs are related. Formal methods provides a smorgasbord of techniques applicable in various ways to the entire software life-cycle. Formal methods can be used for stating requirements, analyzing requirements, specifying code, checking that code specs conform to requirements, analyzing the conformance of source code to specs, analyzing translation of source to object, analyzing the compiled object code, analyzing the hardware on which the object code runs, and more. This broad array of possibilities is just the opposite of a straight jacket.
Mathematical logics necessarily constrain descriptions. If what you need to assert is very difficult to express in a particular logic then you need to consider the possibility that (a) you should shop around for a formalism more appropriate to your task or (b) the mathematical underpinnings for your application are not well enough developed for logical reasoning to be applicable.
If formal methods meant only code-level proofs then its adoption might be considered a straight jacket. Because of the informal mathematical reasoning and testing that good programmers apply to code development, they produce correct software modules on a regular basis. The additional overhead of code proofs could add substantial cost to such modules (using current technology). It might also be very difficult, for example in the case of a program that used floating point. The justification for code proofs on small modules is identical to the justification for any technique: does the assurance required for this application justify the cost of the analysis?