Sidebar
3-9: Formal Methods Can Catch Difficult-to-See Problems
Formal methods are sometimes used to
check various aspects of secure systems. The notion "formal methods"
means many things to many people, and many types of formal methods are proffered
for use in software development. Each formal technique involves the use of
mathematically precise specification and design notations. In its purest form,
formal development is based on refinement and proof of correctness at each
stage in the life cycle. But all formal methods are not created equal.
Pfleeger and Hatton [PFL97a] point
out that, for some organizations, the changes in software development practices
needed to support such techniques can be revolutionary. That is, there is not
always a simple migration path from current practice to inclusion of formal
methods, because the effective use of formal methods can require a radical
change right at the beginning of the traditional software life cycle: how we
capture and record customer requirements. Thus, the stakes in this area can be
particularly high. For this reason, compelling evidence of the effectiveness of
formal methods is highly desirable.
Gerhart et al. [GER94] point out
that
There is no simple answer to the
question: do formal methods pay off? Our cases provide a wealth of data but
only scratch the surface of information available to address these questions.
All cases involve so many interwoven factors that it is impossible to allocate
payoff from formal methods versus other factors, such as quality of people or
effects of other methodologies. Even where data was collected, it was difficult
to interpret the results across the background of the organization and the
various factors surrounding the application.
Naur [NAU93] reports that the use
of formal notations does not lead inevitably to improving the quality of
specifications, even when used by the most mathematically sophisticated minds.
In his experiment the use of a formal notation often led to a greater number of
defects, rather than fewer. Thus, we need careful analyses of the effects of
formal methods to understand what contextual and methodological characteristics
affect the end results.
However, anecdotal support for formal
methods has grown, and practitioners have been more willing to use formal
methods on projects where the software is safety critical. For example,
McDermid [MCD93] asserts that "these mathematical approaches
provide us with the best available approach to the development of
high-integrity safety-critical systems." Formal methods are becoming used
routinely to evaluate communication protocols and proposed security policies.
Evidence from Heitmeyer's work [HEI01] at the U.S. Naval Research
Laboratory suggests that formal methods are becoming easier to use and more
effective. Dill and Rushby [DIL96] report that use of formal methods to
analyze correctness of hardware design "has become attractive because it
has focused on reducing the cost and time required for validation … [T]here are
some lessons and principles from hardware verification that can be transferred
to the software world." And Pfleeger and Hatton report that an air traffic
control system built with several types of formal methods resulted in software
of very high quality. For these reasons, formal methods are being incorporated
into standards and imposed on developers. For instance, the interim U.K.
defense standard for such systems, DefStd 00-55, makes mandatory the use of
formal methods.
However,
more evaluation must be done. We must understand how formal methods contribute
to quality. And we must decide how to choose among the many competing formal
methods, which may not be equally effective in a given situation.
Related Topics
Privacy Policy, Terms and Conditions, DMCA Policy and Compliant
Copyright © 2018-2023 BrainKart.com; All Rights Reserved. Developed by Therithal info, Chennai.