The formal methods model encompasses a set of activities that leads to formal mathematical specification of computer software. Formal metho...
The formal methods model encompasses a set of activities that leads to formal mathematical specification of computer software. Formal methods enable a software engineer to specify, develop, and verify a computer-based system by applying a rigorous, mathematical notation. A variation on this approach, called cleanroom software engineering , is currently applied by some software development organizations.When formal methods are used during development, they provide a mechanism for eliminating many of the problems that are difficult to overcome using other software engineering paradigms. Ambiguity, incompleteness, and inconsistency can be discovered and corrected more easily, not through ad hoc review but through the application of mathematical analysis. When formal methods are used during design, they serve as a basis for program verification and therefore enable the software engineer to discover and correct errors that might go undetected.
Although it is not destined to become a mainstream approach, the formal methods model offers the promise of defect-free software. Yet, the following concerns about its applicability in a business environment have been voiced:
1. The development of formal models is currently quite time consuming and
expensive.
2. Because few software developers have the necessary background to apply
formal methods, extensive training is required.
3. It is difficult to use the models as a communication mechanism for technically
unsophisticated customers.
These concerns notwithstanding, it is likely that the formal methods approach will gain adherents among software developers who must build safety-critical software and among developers that would suffer severe economic hardship should software errors occur.
