Subsections

• Do stronger guarantees of parameter behavior enable stronger framework properties to be validated?
• What analysis techniques can be effectively applied to frameworks and the components that parameterize and use them?
• What is the cost vs. effectiveness tradeoff of framework analyses?
• How best can the results of framework validation and parameter assumptions be presented and reused by framework consumers?

Analysis of Software Frameworks

Do stronger guarantees of parameter behavior enable stronger framework properties to be validated?

Frameworks make assumptions about their parameters. Practitioners of formal methods are free to model these assumptions in a variety of safe ways, i.e., by weakening the actual assumption. Usually we want to use the weakest possible assumptions because they provide the broadest degree of applicability for the reasoning result, i.e., those assumptions are satisfied in more contexts that use a framework. Given this range, can stronger parameter assumptions be put to good use?

What analysis techniques can be effectively applied to frameworks and the components that parameterize and use them?

Once we understand the range of formal specification methods that can be applied to frameworks and the components that interact with, then we want to understand what reasoning techniques are applicable. Can fully-automated techniques such as model-checking, flow analyses, and state-space search methods be applied to those portions of the problem for which lighter-weight methods are appropriate? Can these techniques be effectively integrated, where necessary, with reasoning techniques for heavier-weight methods?

What is the cost vs. effectiveness tradeoff of framework analyses?

This is really an empirical question. It should be clear that using an exact form of reasoning is infeasible. We are then left with performing an approximating analysis to reason about behavior; to the extent that such an analysis is safe or conservative we will be able to trust (some of) its results. Given this and considering the application of such methods to realistic software frameworks: Can limiting the scope of analysis to the framework effectively reduce validation cost? Do we actually reduce run time? Can limiting scope of analysis to the framework preserve sufficient levels of accuracy in their results? Do we get trustworthy results, i.e., that are as meaningful as a proof.

How best can the results of framework validation and parameter assumptions be presented and reused by framework consumers?

We could simply bundle specifications as text with the source code of a framework and satisfy the desire for precise documentation of frameworks. We could link parameter specifications with appropriate verification tools so that they could be invoked at framework instantiation time. What level of expertise will be required of consumers of this kind of capability? What about tools that require some kind of user interaction?