Contracts for Software Product Lines

The verification of product lines is an active research area (see a recent survey). Verification techniques such as model checking, theorem proving, or static program analyses are adopted to software product lines. All these effort to scale verification techniques to product lines are typically evaluated against a brute-force strategy (i.e., the verification of each single product), but not with each other. Comparability is often not given as each verification technique is based on a different specification technique.

In design by contract, object-oriented programs are specified by means of method contracts and class invariants (for short contracts). We propose to apply contracts to product lines for several reasons. First, contracts are code-level specifications that can be used for many verification techniques and even testing, making them comparable. That is, we can apply several verification techniques to the same product line's code base and specification. Second, if we study contracts in product lines, we can judge about specification techniques on more abstract levels.

Product-Line Verification with Contracts

Variability encoding is an elegant technique to reuse verification techniques from single-system engineering for product-line engineering. The main idea is to convert compile-time variability into runtime variability within the input language of the verifier. In our GPCE'12 paper, we showed how to apply variability encoding not only to source code, but also to contracts, and how to reuse the existing theorem prover KeY as-is for product-line verification. The result of transforming compile-time into runtime variability is a metaproduct. The idea of variability encoding is to reduce the verification of each single product to the verification of the metaproduct, consisting of a metaprogram and a metaspecification.

Contracts in FeatureIDE

We extended FeatureIDE with support for contracts in feature-oriented programming. In this course, we extended FeatureHouse with support for parsing and pretty printing JML contracts. Furthermore, contracts can be composed during the composition of feature modules resulting in contracts in generated products. Beyond this, we implemented variability encoding in FeatureHouse supporting Java-like feature modules and JML-like contracts.

Both, the FeatureIDE and the FeatureHouse extension are integrated in the respective main branch. The overall tool support is available in FeatureIDE 2.7.0.

We prepared screencasts for some functionality of FeatureIDE with respect to contracts:

Experiment with the BankAccount Product Line

For our experiment with model checker JPF and theorem prover KeY, we provide the product line's source code (i.e., the BankAccount product line), the source code for mutation generation, and raw data for replication.