No one method or tool can serve all purposes. We need to support all
different kinds. From past experience, we have learned what kinds can
have the most impact.
To be attractive to practitioners, methods and tools should satisfy
the following criteria. We realize that some of these criteria
are ideals, but they are still good to strive for.
- <#259#>Early payback<#259#>.
Methods and tools should provide significant benefits almost as soon as people
begin to use them.
- <#260#>Incremental gain for incremental effort<#260#>.
Benefits should increase as developers get more adept or put more effort into
writing specifications or using tools.
- <#261#>Multiple use<#261#>.
It should be possible to amortize the cost of a method or tool over many uses.
For example, it should be possible to derive benefits from a single
specification at several points in a program's life cycle: in design analysis,
code optimization, test case generation, and regression testing.
- <#262#>Integrated use<#262#>.
Methods and tools should work in conjunction with each other and with
common programming languages and techniques. Developers should not
have to ``buy into'' a new methodology completely to begin receiving
benefits. The use of tools for formal methods should be integrated with
that of tools for traditional software development, e.g., compilers and
simulators.
- <#263#>Ease of use<#263#>.
Tools should be as easy to use as compilers, and their output should be as easy
to understand.
- <#264#>Efficiency<#264#>.
Tools should make efficient use of a developer's time. Turnaround
time with an interactive tool should be comparable to that of normal
compilation. Developers are likely to be more patient, however, with
completely automatic tools that perform more extensive analysis.
- <#265#>Ease of learning<#265#>.
Notations and tools should provide
a starting point
for writing formal specifications
for developers who would not otherwise write them. The knowledge of formal
specifications needed to start realizing benefits should be minimal.
- <#266#>Error detection oriented<#266#>.
Methods and tools should be optimized for finding errors, not for certifying
correctness. They should support generating counterexamples as a means
of debugging.
- <#267#>Focused analysis<#267#>.
Methods and tools should be good at analyzing at least one aspect of a
system well,
e.g., the control flow of a protocol. They need not
be good at analyzing all aspects of a system.
- <#268#>Evolutionary development<#268#>.
Methods and tools should support evolutionary system development by allowing
partial specification and analysis of selected aspects of a system.
More ambitiously, rather than build a single tool, we can
build ``meta-tools'' which themselves produce tools customized for a
particular problem domain~[#SMCB96##1#], formal notation~[#pac##1#], or
logic~[#hol##1#, #kindred-wing96##1#]. These meta-tools, like compiler
generators, provide an automatic way to build specialized model checkers or
proof checkers.
Finally, for any new method or tool, its developer should state explicitly what
its strengths, limitations, modeling assumptions, ease of integration
with other methods and tools, and start-up costs are. Clear selection
criteria help potential users decide what method or tool is most
appropriate for the problem at hand.