Why Study Formal Methods in Software Engineering?

The software industry has a long standing and well earned reputation for failing to deliver on its promises. In the September 1994 issue of Scientific American, a number of sobering examples are given and it is observed that "despite 50 years of progress, the software industry remains years -- perhaps decades -- short of the mature engineering discipline needed to meet the needs of an information-age society." In an article in the January/February 1997 issue of I.E.E.E. Software, Luqi and Goguen cite staggering cost estimates of software development failures at $81 billion for 1995, and $100 billion for 1996. In his Web article, Goguen calls attention to several highly visible failures: the cancellation of IBM's $8 billion contract with the FAA for a new nation-wide air control system, the DOD cancellation of a $2 billion contract with IBM to modernize its information systems, the failure of the software for delivering real-time sports data at the 1996 Olympics, the one and one-half year delay in the United Airlines automated baggage handling system at the new Denver airport at a cost of $1.1 million per day, and the list could go on. A reading of Peter Neumann's book, Computer Related Risks, will reveal that such problems are not at all new, although they appear to be growing. Neumann even points out deaths which resulted from radiation overdoses from a computer-based radiation-therapy system in the mid-1980s

It is clear that there is no price that can assure the success of software projects with the current technology. For large complex projects an ad hoc approach has proven inadequate. The lack of formalization in key places makes softeware engineering overly sensitive to the foibles that are inevitable in the highly technical and detailed activities associated with software creation. Aids to precision and cross-checking are essential, and this is precisely the objective of formal methods.