Contribution to the Panel Discussion: Formal Methods after Fifteen Years
(FORTE'95, Oct. 1995, Montreal)

The Trend Toward Application-Specific Research

The Trend and Its Probable Origin

In the formal-methods research community, there seems to be a trend away from general methods and tools--those that are supposed to apply equally well to all software. The trend is toward methods and tools that address the particular characteristics and problems of specific application domains.

To some extent, this trend is externally imposed. These are lean times for research funding, and research with obvious practical value has a better chance of getting support. In formal-methods research, by far the easiest way to show practical value is to work on a specific application domain. Even a negative result is useful, because it shows practitioners within that application domain what not to waste their time on!

Despite the negative aspects of this motivation, the trend is good for research in formal methods. The next two subsections give two reasons why it will lead to stronger and more interesting (as well as more useful) research results.

"Software Engineering" Is "Physical Engineering"

When we compare software engineering to civil, chemical, aeronautical, nuclear, electrical, mechanical, and biomedical engineering, we can see that software engineering is the software aspect of "physical engineering" [10]. No other engineering discipline is related to so many different parts and aspects of the real world.

For the same reason that there is no major in Physical Engineering, it is unrealistic to expect that excellent software can be built for all application domains using the same tools and techniques. Application-specific research thus moves us in a more productive direction.

It is also somewhat arrogant for us to assume that it is possible to make a contribution to software development in an application domain without extensive knowledge of the nature of that application domain. A field study of the software design process [11] showed that "exceptional designers" stand out because of their domain knowledge:

• ". . . these individuals had remarkable control over project direction and outcome, and in some cases [were] described by others as the person[s] who `saved' the system."
• "Exceptional designers performed broader roles than design, and were recognized as the intellectual core of the project (i.e., the keeper of the project vision) by other project members."
• ". . . exceptional designers were extremely familiar with the application domain. Their crucial contribution was their ability to map between the behavior required of the application system and the computational structures that implemented this behavior . . . ."
• For large embedded systems these problems are complicated by the number of domains that must be integrated. For instance, designing military avionics software might require expertise in flight control, navigation, sensor-data processing, electronic countermeasures, and target acquisition."

Example of a Research Problem: Description Complexity

One of the major unsolved problems in formal methods is the size and complexity of formal descriptions of real systems. Only three basic attacks on this problem come to mind:

1. Module Reuse: A description of size x, used y different times, reduces the total size of the description by (y-1)x.
2. Layers of Interpretation: A description that is interpreted or translated into some lower-level form can be dramatically smaller than a corresponding uninterpreted description. For example, a grammar is a very concise description of a parser. It is converted to a much larger, executable program by a parser generator. Also, macro expansion is a simple example of translation from a smaller, more specialized description to a larger description in a more general form.
3. Separation of Concerns: Consider a system that is described in two orthogonal views, one of size x and one of size y. Since the views are orthogonal, almost any "feature" of the x view can combine with almost any "feature" of the y view, and together they describe behavior that would require an undecomposed description of size xy. Yet the decomposed description is of size x+y.

These three strategies have been studied extensively. We can divide research on these strategies into two categories. The first category concerns general-purpose, technical support of the strategies. The second category concerns applying them creatively and productively to application domains.

The point of this example is that, when we look at each of the three strategies, research on technical support is much more mature than research on applications. In other words, there is much more room for innovative work on applications. Furthermore, some of the most useful and intellectually satisfying results are those in which a strategy has been applied cleverly to an application domain.

Table 1 shows examples of research topics or results in each of the six divisions, and gives an estimate of the maturity or saturation of research in that division. Maturity estimates range from 5 (very mature) to 1 (very new and open).

[Table 1: see ps file]