ARTICLE SUMMARY
The software crisis continues to worsen with no immediate end in sight
to the problems of producing correct and reliable software for the size
of software-based systems that are now required and expected by
customers. We are suffering from a "plague of bugs" of biblical
scale.
Many techniques have been suggested for the alleviation of the symptoms
being experienced in the software industry. One that holds some hope is
the application of formal methods. These provide a rigorous
mathematical basis to software development, allowing formalization of
the system being designed in the form of a mathematically precise
specification much earlier on in the design cycle than is currently
usually the case. This allows the discovery of bugs, particularly in
the requirements where the majority of errors tend to reside in
practice, much earlier than the coding stage, or even worse and far
more expensively, when the software is out in the field, where they are
typically discovered at present.
Much research has been aimed at the improvement of the foundations of
formal methods. While this is extremely important, equally important
for the technology transfer process is the provision of advice on how
such methods can be applied in an industrial setting. It is, quite
rightly, widely accepted that there is no "silver bullet" which will
solve the software development problem. However this article offers a
"golden ark" of "commandments" or maxims together with some relevant
explanatory information. This advice, while in no way guaranteeing the
successful use of formal methods will, we hope, help to avoid some of
the common pitfalls in their application.
Jonathan P. Bowen and Michael G. Hinchey. Ten Commandments of Formal Methods, IEEE Computer, 28(4):56-63, April 1995. Previous version available as Technical Report No. 350, University of Cambridge Computer Laboratory, 18pp, September 1994.