NASA Langley Research Center has, for eight years, conducted and sponsored research to develop formal methods for high integrity applications. For the past four years, Langley's effort has focused primarily on projects to inject formal methods technology into commercial use. In particular, NASA Langley has sponsored SRI International to work with Rockwell Collins to formally verify a portion of the AAMP5 microprocessor, and fully verify the AAMP-FV, which is a new microprocessor being developed by Collins for potential use in critical applications. We have also funded Odyssey Research Associates to work with Honeywell Air Transport Systems to develop formally based tools and techniques to analyze and manipulate decision table specifications. Other projects have applied formal methods to fault-tolerant algorithms developed by Allied Signal, advanced control algorithms under development by Union Switch and Signal, and change requests to space shuttle software.
All of these projects have met the goals we established for them. In fact, they have often been cited as good examples of industrial use of formal methods. Nevertheless, these projects have also illustrated that there remain serious impediments to the full acceptance of formal methods by industry. Some of the impediments frequently cited by the formal methods community include such industrial problems as inadequately educated engineers, the not-invented-here syndrome, and greater emphasis on reducing costs than on increasing safety. However, we believe that the primary causes for the lack of wide-scale industrial use of formal methods are (1) inadequate tools, (2) inadequate examples, and (3) a "build it and they will come" expectation. The projects cited above have succeeded because our partners have been able to overcome or avoid these pitfalls in one way or another. In the rest of this article, we will discuss each of the three factors, and provide suggestions as to what formal methodists can do to overcome them.
Tools. Inadequate tools are a serious impediment to industrial use of formal methods. Almost all formal methods researchers will acknowledge that most existing tools are not production-quality and are difficult to learn to use effectively. Not only do the input languages use specialized notations from mathematical logic, but many tools have numerous bugs in them. Few things are more disconcerting to formal methods neophytes than having to wonder constantly if their inability to complete a proof is a result of their own lack of skill, the falsity of what they are trying to prove, or a bug in the tool. Prototype tools must be built, but no one should expect such tools to be used regularly within industry.
One cause for optimism is that many of the formal method tool developers are working on their third- or fourth-generation tools. Some of these evolving tools are also being developed with industrial use as a major goal and are being applied to increasingly sophisticated real problems. Also, government sponsors are working to build cooperation between different projects so that the methods and tools developed at different sites work together. This will also help reduce some of the duplication of effort that has unfortunately characterized the field.
Despite our optimisim, increased vigilance is still needed on several fronts. Tool developers must curb their desires to create more and more powerful tools, and instead expend increased effort on improving the robustness and performance of existing tools. The emerging tools should be thoroughly exercised within the formal methods community before they are made available to industry; government sponsors can take a large role in this area. Finally, when tools are made available to industry, formal methods experts must be available to provide guidance in the tool's use and ways to overcome its shortcomings. There is a growing need for training courses that are tailored for industrial users.
Inadequate Examples. A second impediment to industrial use of formal methods is the inadequacy of existing examples and models. For too long, formal methods researchers have worked on toy examples and intellectually interesting but industrially irrelevant problems. Although academic-style work is essential to the advancement of the field, it cannot be the only work that is done. Because so few researchers have concentrated on industrially relevant problems, most of the examples and models that have been developed have borne little resemblance to the examples and models needed in industry.
We cannot expect industry to develop the needed models alone. The first attempt to formalize a new problem domain requires a significant time investment, one that is almost always longer than engineers with product deadlines can afford to make. The time required to formalize the underlying domain-specific knowledge in existing formal verification tools can be considerable, but this is often not recognized even by formal methodists until they tackle a real application. Also, the first endeavor in a new domain requires far greater creativity than subsequent efforts.
The solution to this impediment is conceptually simple: more formal methods researchers must become knowledgeable about the problem domains that are relevant to industry, and develop examples, models, techniques, and tools appropriate for those domains. This means that some formal methodists must be willing to tackle problems that are not intellectually interesting but that industry needs solved. It also means that some must be willing to forgo using powerful and sophisticated methods, when simple and pedestrian ones will suffice. Much of the success of NASA Langley's program can be attributed to our contractors' willingness to attempt to understand important problem domains such as fault-tolerant computing, clock synchronization, flight control and management, and microprocessor design. Also, we have tackled mundane and tedious problems when necessary; and our contractors have created simple, special-purpose tools, when such tools were sufficient to meet the needs of the customer.
"Build it and they will come." The final impediment to industrial use of formal methods is the expectation that if one builds an advanced tool, it will be used. This viewpoint overlooks the gulf that exists between the research world and the industrial world. Industry rarely has the time and resources to keep up with and distill the vast number of ideas and tools that are emerging from the research community, and the research community is often ignorant of the challenges that industry faces. Literally hundreds of different kinds of formal methods have been promoted, but we lack adequate executive-level guidance on how to match particular methods with specific applications, and few unbiased appraisals exist of the maturity of current methods and tools.
Furthermore, the gulf between academia and industry has been widened by the rhetoric of some formal method zealots who blame industry for its failure to embrace formal methods and question the intellectual acuity of industry engineers. These zealots have also exaggerated the importance of formal methods by claiming that only formal methods can prevent future catastrophes, and by telling industry that formal methodists know better than professional engineers how to build real systems.
The solution to this impediment is also conceptually simple: formal methods researchers must stop giving answers and start asking questions. Instead of saying, "We know what you're doing wrong and how to fix it," we should be asking, "Where are you having trouble and what can we do to help you?" If the potential benefits of formal methods are as great as those of us in the field believe, then we should be able to demonstrate those benefits by dispassionate logic and empirical data. In short, we need more ambassadors and fewer warriors.
The three major impediments listed above can be overcome. We believe that NASA Langley's sponsorship of ground-breaking uses of formal methods in several domains has helped to show how this can be done. We hope that continued government sponsorship---from NASA Langley and from other sources---will help speed the process.
Ricky W. Butler is a senior research engineer at the NASA Langley Research Center. He leads the Formal Methods Team in the Flight Electronics Technology Division. His research is on the application of formal methods to high-integrity systems with particular focus on fault-tolerant architectures used for flight control and flight management. E-mail: r.w.butler@larc.nasa.gov