Safety-critical systems should require a formal methods specification
John Cuadrado
A plane from a major airline crashes, killing everybody aboard. After many months of investigation, the responsible authorities declare that the accident might have been caused by a faulty component in the plane's fly-by-wire system. Months pass; eventually the families of some of the victims sue the airline for damages. During the trial, the attorneys for the victims' families produce an analysis of the logic of the fly-by-wire system that reveals several previously undetected fault modes. These modes are shown to be directly responsible for the plane's crash. Not only does the judge award the families a substantial sum of money, but he or she also starts proceedings to have the plane's manufacturer charged under a new cri
minal negligence statute.
Such a scenario may occur in the near future. Several European and Canadian agencies have issued new guidelines strongly recommending--and in some cases mandating--the use of formal methods and proof in the development of hardware and software for safety-critical systems (e.g., nuclear reactor and military systems).
At the present time, the situation is different in the U.S. Under pressure from many manufacturers, the U.S. government has been reluctant to follow the lead of some European countries in recommending the use of formal methods in the development of safety-critical systems. These manufacturers have a misguided fear of the difficulty and the costs involved in using formal methods.
For the past 30 years, a large body of material on formal methods has been accumulating at research institutions. For over 15 years, several introductory texts have taught the use and practice of formal methods.
The main idea of a formal specification is to use a formal la
nguage to describe a set of properties that the underlying system must satisfy. This implies that there are at least two formal languages. One is used to describe the properties we are trying to specify; another (possibly the same) language describes the system about which these properties are to be verified. The languages themselves need to be formally defined.
There are many such languages and techniques, ranging from various logics to algebraic models. Many systems provide automatic tools for the composition of formal specifications and several semiautomatic theorem provers for the verification of such specifications.
Although much work remains to be done, particularly in the area of distributed systems, there is a solid core of materials available for systems developers. There is also the issue of the current set of programming languages available for the coding of what has been specified using a formal language. Ideally, implementation languages would facilitate the verification of system p
roperties. For example, in some Prolog-like languages, we come close to having executable specifications: The formal description of what the system is to accomplish can be written in the same underlying logic language.
The main complaint one hears from industry is that it is almost impossible to hire people who are trained in the use of these techniques. Training in the use of formal methods must become an integral part of the computer science curriculum before there is any hope of these techniques being applied in industry. These methods are not any more difficult than the differential equations and vector analysis techniques that all engineers learn in their undergraduate education. Training has to begin with the first course in computer science and continue to be used and enhanced during a scientist's professional life.
Most U.S. colleges require their students in engineering and science to take many ``service'' courses in mathematics. These include three semesters of calculus and one semeste
r of differential equations. Most computer science majors won't use the majority of these techniques. It would be much more useful to teach these students the logic and algebraic methods that can be immediately applied in their chosen discipline.
In the U.S. today, there is a large pool of well-educated, mature scientists from what used to be the defense industry. Many of these individuals have advanced degrees in math, physics, electrical engineering, and other technical areas. It would be simple to teach them the formal methods approach to software and hardware development. These people could be hired and used as catalysts for the growth of formal techniques in U.S. industry. What an opportunity for some smart politician!
John Cuadrado is an independent consultant in Maine. His primary areas of interest include distributed database systems, applied AI, and theories of parallel computation. You can reach him on the Internet or BIX c/o
editors@bix.com
.q
Teach Formal Methods
