The decision to use of formal methods in the real world is not one that is taken lightly. Bowan and Hinchley have coined “the ten commandm...
The decision to use of formal methods in the real world is not one that is taken lightly. Bowan and Hinchley have coined “the ten commandments of formal methods” as a guide for those who are about to apply this important software engineering approach.
1. Thou shalt choose the appropriate notation. In order to choose effectively from the wide array of formal specification languages, a software engineer should consider language vocabulary, application type to be specified, and breadth of usage of the language.
2. Thou shalt formalize but not overformalize. It is generally not necessary to apply formal methods to every aspect of a major system. Those components that are safety critical are first choices, followed by components whose failure cannot be tolerated (for business reasons).
3. Thou shalt estimate costs. Formal methods have high startup costs. Training staff, acquisition of support tools, and use of contract consultants result in high first-time costs. These costs must be considered when examining the return on investment associated with formal methods.
4. Thou shalt have a formal methods guru on call. Expert training and ongoing consulting is essential for success when formal methods are used for the first time.
5. Thou shalt not abandon thy traditional development methods. It is possible, and in many cases desirable, to integrate formal methods with conventional or object-oriented methods . Each has strengths and weakness. A combination, if properly applied, can produce excellent results.
6. Thou shalt document sufficiently. Formal methods provide a concise, unambiguous, and consistent method for documenting system requirements. However, it is recommended that a natural language commentary accompany the formal specification to serve as a mechanism for reinforcing the reader’s understanding of the system.
7. Thou shalt not compromise thy quality standards. “There is nothing magical about formal methods” and for this reason, other SQA activities must continue to be applied as systems are developed.
8. Thou shalt not be dogmatic. A software engineer must recognize that formal methods are not a guarantee of correctness. It is possible (some would say, likely) that the final system, even when developed using formal methods, may have small omissions, minor bugs, and other attributes that do not meet expectations.
9. Thou shalt test, test, and test again. Formal methods do not absolve the software engineer from the need to conduct well-planned, thorough tests.
10. Thou shalt reuse. Over the long term, the only rational way to reduce software costs and increase software quality is through reuse. Formal methods do not change this reality. In fact, it may be that formal methods are an appropriate approach when components for reuse libraries are to be created.
