What is the problem?

Parameterizeable programming frameworks are becoming widely available to support developers in complex software domains. The strength of these frameworks is that they hide significant amounts of detail behind relatively simple interfaces. As with most software systems, validating a framework is typically done through a process of testing. Since a framework is not a complete application, it is necessary to construct a potentially elaborate collection of stubs and drivers to fill the roles of framework parameters and callers in order to test. Unlike for traditional applications, in testing frameworks the test designer may have little information about the potential behavior of framework parameters. Thus, one's ability to do a ``good job'' of testing may be reduced.

The problem for users of frameworks is determining whether the testing and validation efforts and results for a framework are representative of the context in which they wish to apply the framework. In other words, do traditional state-of-the-practice techniques for framework validation enable reuse and application of validation information in the context of systems built with the framework. Some researchers have addressed this problem for sequential reusable components by using formal specifications and developing proof methods that enable local certifiability of those components [WH94]. This approach takes the traditional formal methods approach of providing and reasoning about complete specifications of component behavior. In contrast, we believe that an approach based on partial specifications can yield a number of advantages. It offers the potential for practical fully-automated verification, via techniques such as model checking. It can address properties of both sequential and concurrent software frameworks; this is important because concurrent systems are very difficult to construct and to validate. It can be used to reason about a wide-range of correctness properties of systems (although there are properties that cannot be handled). We believe that an approach which adapts existing work on finite-state verification using the idea of local certifiability can bring the benefits of fully-automated verification without suffering from the well-known state explosion problem.

Such an approach decomposes framework validation into two steps:

1.

Framework developers reason about correctness of frameworks in isolation

2.

Framework users leverage those reasoning results for applications of framework

This decomposes the validation problem along boundaries that are similar to the design and implementation boundaries developers are familiar with. In this way it allows for separation of validation concerns. This approach raises a number of interesting research questions, which we present below.