Here is an HTML version of an article I wrote on my own time related to this subject.
One of the most basic questions anyone can ask is, "How do I know that what I think I know is true?" The study of this question is called epistemology. Traditionally, epistemology has been considered to be of legitimate interest only to philosophers, theologians, and three-year-old-children, who respond to every statement by asking, "Why?" Software engineers need to be interested in the subject, however, because a lack of sufficient understanding of epistemology contributes to many of the current problems in the field.
Epistemology is a complex subject, one to which many philosophers and theologians have devoted their entire careers. The discussion here is necessarily brief and incomplete; however, it should be sufficient to demonstrate the critical importance of the subject to software engineering.
To the fundamental question of how do we know what is true, there are three basic answers: authority, reason, and experience. An epistemology based on authority states that truth is given to us by someone more knowledgeable than ourselves. The two primary variations of authority-based epistemologies are omniscient authority (the authority is God), and human authority (the authority is a human expert).
An epistemology based on reason claims that what is true is that which can be proven using the rules of deductive logic. Finally, an epistemology based on experience claims that what is true is that which can be encountered through one or more of the senses.
Several different variations of experience-based epistemologies exist. The two variations relevant to this discussion are anecdotal experience and empirical evidence. The first states that truth for any particular individual or group of individuals is that which the individual, or group, personally experiences. The second states that truth is that which can be verified through carefully controlled experiments.
The relative strengths of these epistemological approaches are as follows. Omniscient authority provides absolute truth; if there is a God and He has spoken on something, then what He says must, by definition, be true. Reason yields conditional absolute truth; if the premises on which a valid deductive argument are known to be true, then the conclusion of the argument must also be true.
Empirical evidence provides probable truth; if controlled experiments are designed properly and repeated enough times, then it is highly probable that the results accurately describe reality. Anecdotal experience yields possible truth; if something happened for one person, it is possible it might happen to others also. Finally, human authority provides opinion.
On which of these approaches to epistemology is software engineering mostly based?
The software engineering literature is filled with pronouncements about how software should be developed (e.g., "Object-oriented development is the best way to obtain reusable software"). Rarely, if ever, are these pronouncements augmented with either logical or experimental evidence. Thus, one is forced to conclude that much of software engineering is based on a combination of anecdotal experience and human authority. That is, we know that a particular technique is good because John Doe, who is an expert in the field, says that it is good (human authority); John Doe knows that it is good because it worked for him (anecdotal experience). This is a weak epistemological foundation on which to base an entire discipline.
This current state should not be surprising; the development of software engineering is following the same pattern as the development of many other disciplines. Civil engineering, chemical engineering, aeronautical engineering, and others all had periods in which they relied almost exclusively on anecdotal experience and the subsequent authority of the "experts". Often, it took major disasters before practitioners in such fields began to investigate fully the foundations on which their field was based.
To date, although there have been many, many software problems, there have been no major disasters that have been directly attributed to software. However, unless a sound epistemological foundation is established for software engineering, disasters will come one day. To avoid this, research is needed to develop valid approaches to answering questions about both software products (e.g., are these requirements consistent?) and software processes (e.g., is method A better than method B?).
The Assessment Technology Branch (ATB), which is part of the Information and Electromagnetic Technology Division, Research and Technology Group, is currently investigating empirical methods to answer process-type questions and logical methods to answer product-type questions. The remainder of the presentation discusses the second of these two avenues of research.
A team led by Ricky W. Butler has been studying the discipline of formal methods for over 6 years. Other civil-servants on the team are Jim L. Caldwell, Victor A. Carreño, C. Michael Holloway, and Paul S. Miner. Vigyan, Inc., Stanford Research Institute International (SRI), Odyssey Research Associates (ORA), and Computational Logic, Incorporated (CLI) conduct research under contract.
Formal methods is the applied mathematics of computer systems engineering. Formal methods aims to be to software engineering what fluid dynamics is to aeronautical engineering and what classical mechanics is to civil engineering. The mathematics of formal methods includes predicate calculus (first order logic), recursive function theory, lambda calculus, programming language semantics, and discrete mathematics (e.g., number theory, abstract algebra). To this mathematical base, formal methods adds notions from programming languages such as data types, module structure, and generics.
There are many different types of formal methods with various degrees of rigor. The following is a useful classification of the possible degrees of rigor in the application of formal methods:
Presently, a complete (level 3) verification of a large, complex system is impractical; however, application of formal methods to critical portions of a system is practical and useful.
The specification of a simple phone book provides a suitable simple example of many of the basic ideas and benefits of formal methods. Please see the presentation visuals that follow this abstract for this example.
Because of the promise that formal methods offers, a considerable amount of high-quality research is being conducted or sponsored by ATB. This research includes, but is not limited to, the following projects:
In addition to these, and other, projects, the branch conducts periodic workshops on formal methods. Previous ones were held in 1990 and 1992; the next one is planned for 1995. Also, an extensive collection of information on the research is available through the World Wide Web at the following Universal Resource Locator:
http://atb-www.larc.nasa.gov/fm-top.html
Interested individuals are encouraged to explore this collection.
A lot of ground has been covered in this presentation, but the most important point is simple: