Formal Methods
``A Strategic Advantage Analysis of Formal Methods in Software
Engineering,''
by
N. Eickelmann and D.J. Richardson, June 1994
Abstract
Software engineering is a relatively young engineering discipline that
is rapidly becoming of central importance in our technology driven
society. The disparity between the maturity of software engineering as
a discipline and the scope of its central role in society must be
addressed. Software engineering is responsible for the development of
large, complex software that is often safety-critical or
security-critical in nature. However, current practice does not
provide the same level of rigor and formality in developing its
products as is used by other engineering professions.
This problem may be addressed by applying formal methods, whose
logical constructs and mathematical models provide a sound
mathematical foundation for software engineering practice. It would be
presumptuous to assume formal methods can address every problem, as it
would be inappropriate to disregard the empirical evidence of their
value. This paper analyzes current practice of formal methods and
characterizes viable strategies to optimize their impact. Formal
methods strategically applied may facilitate software engineering in
its ability to predict and control its development process as well as
its product.
This paper analyzes formal methods using a Strategic Advantage
Analysis model. The model provides a framework for systematic,
evaluative analysis, which is inherently a risk assessment applied to
the unique factors relevant to formal methods. The analysis is
approached from three diverse perspectives, the academic community,
the software industry, and governmental agencies. The three
perspectives are complementary and are used to identify key areas of
strategic advantage, including reuse, reengineering, and
hardware/software codesign. Strategic application of formal methods
may provide leverage to advance software engineering.
Keywords
Formal methods, formal frameworks, mathematical models,
programming-in-the-large (PITL), reuse, reengineering, software quality.
from Debra J. Richardson
djr@ics.uci.edu
Department of Information and Computer Science,
University of California, Irvine CA 92717-3425