Anyone who has tried to use an operating system or application only to encounter a show-stopping error understands that software and computer systems are highly imperfect. Such users would be correct in imagining, perhaps after beholding the classic “Blue Screen of Death,” that the development of such technology is an imprecise affair that involves a great deal of empirical testing. In other words, developers fix errors as they occur, and may not even know their initial cause. There is, however, a slow, exacting alternative to empirical testing call “formal methods,” whereby the programmer maps out the course of a computer program like an architect maps out the design of a building.
This page provides an introduction to formal methods for computer users with only a modest technical background, including students who might be considering a career in software engineering or development. The links provided throughout the sections below are generally geared toward an academic and tech-savvy audience, although they were selected because much of their content is still accessible to lay readers, allowing them to to ease into this often-intimidating subject matter.
Formal Methods Defined
Normal development of software, hardware, and whole computer systems is largely a matter of trial and error. Programmers design software applications, for example, with bug-catching procedures in order to eliminate as many of the inevitable errors as possible. This process is uneven, and developers expect to release software to the public with known bugs, a necessity given how complex computers have become. In the early years of computing, however, it was possible to painstakingly describe a program’s every decision using a formal, strictly logical, mathematical system of notation, or “specification language” (see Professor Curt Clifton’s presentation on the subject) and thus identify errors before they occur. These are formal methods.
Normally the process of mapping out an entire program before writing the actual code would be needlessly time-consuming and expensive for the development of, say, a word processor or video game. However the program that controls a passenger jet’s artificial horizon, a bank’s security system, or a city’s traffic light framework could result in deadly or economically costly consequences if errors are not eliminated early in the development process. Formal methods are a reliable means of heading off these errors. They allow the programmer or mathematician, by literally writing out a program in rigorous mathematical notation before coding it, to ask questions that would not otherwise occur to him/her until much later, after some errors are irreparable. Details of how a developer might go about using formal methods can be found in Jonathan P. Bowen and Michael G. Hinchey’s advice guide on the subject.
The page, What is Formal Methods? from NASA, concurs with the Formal Methods Group of the University of Toronto in stating that formal methods are often impractical today because of the enormous complexity of modern computer systems, and are therefore only applied to specific parts of hardware or software. However, Formal Methods Europe maintains that the overall cost is not substantially different from other quality assurance procedures. While formal methods cost more during the earlier, “drawing board” phase of a piece of software or computer hardware, they identify errors much earlier on and prevent the steady release of “patches” after a product has been published, thus saving time and money. Software engineer Anthony Hall agrees, demonstrating how the cost of correcting an error late in the process is substantially more than carefully using formal methods from the start. A paper by Martin Gogolla from the University of Bremen looks at both sides of the issue.
Applications of Formal Methods
Today, formal methods are normally applied only in situations where life and death, and large sums of money, are at stake, such as in military equipment. However, this methodology has fervent advocates in a variety of industries who posit that formal methods ultimately reduce costs in the long-term because software applications designed formally require much less maintenance. Some of these industries are described below:
In avionics, the electronic components of aircraft (and spacecraft) must give accurate readings of altitude, speed, pitch, and other critical data, particularly in bad weather or a night when a pilot’s vision is insufficient to make safe decisions. The technology company,
, explains how formal methods can be applied in this industry.
Medical equipment, such as heart monitors, must be able to recognize when a patient has entered critical condition. A paper on the practicality of formal methods in the development of medical devices from a variety of academic (Carnegie Mellon University) and corporate (Varian Medical Systems, Kestrel Technology) contributors is provided
Simulations, according to
, can benefit from “lightweight” formal methods that camouflage some of the innate complexity of the process and provide quick feedback to developers. The applications they have in mind are computer models for hardware, the behavior of whole populations, and NASA space missions.
Information security, in particular the integrity of data on a company’s computer system, requires a great deal of care. James G. Williams and Marshall D. Abrams show how formal methods can be used in a number of models for computerized security systems in
of the book, Information Security: An Integrated Collection of Essays.
is an organization that facilitates the exchange of research between professionals about the titular subject. To do this, they provide regular symposia and offer both news and reports on numerous other meetings throughout Europe.
, although a collection of user-generated content, has a enormous number of external links to sites about the topic. These include individual projects, conferences, introductions, and associations.
is a list of over a dozen online books available from FreeTechBooks.com. Among the titles are
by Frank Pfenning and
by E.C.R. Hehner.
of the University of Manchester maintains a list of tools produced at the school. These include theorem-provers and utilities that streamline some of the more time-consuming aspects of formal methods.
Image is from Ysangkok.