Summary Software product lines enable developers to derive similar products from a common code base. Existing implementation techniques can be categorized as composition‐based and annotation‐based approaches, with both approaches promising complementary benefits. However, annotation‐based approaches are commonly used in practice despite composition allowing physical separation of features and, thus, improving traceability and maintenance. A main hindrance to migrate annotated systems toward a composition‐based product line is the challenging and time‐consuming transformation task. For a company, it is difficult to predict the corresponding costs, and a successful outcome is uncertain. To overcome such problems, a solution proposed by the previous work is to use a hybrid approach, utilizing composition and annotation simultaneously. Based on this idea, we introduce a stepwise migration process from annotation‐based toward composition‐based approaches to lower the adoption barrier of composition. This process itself is independent of used implementation techniques and enables developers to incrementally migrate toward composition. We support our approach with detailed examples by partially migrating a real‐world system. In detail, we describe the following: (1) our migration process, (2) its application on a real‐world system, and (3) discuss practical challenges we face. We implemented the proposed approach and show that appropriate tool support helps to migrate toward composition‐based product lines. Based on the case study, we show that the hybrid product lines work correctly and can compete with the performance of the original annotated system. However, the results also illustrate open issues that have to be solved to apply such migrations in practice.

Today's software systems are often customizable by means of load-time or compile-time configuration options. These options are typically not independent and their dependencies can be specified by means of feature models. As many industrial systems contain thousands of options, the maintenance and utilization of feature models is a challenge for all stakeholders. In the last two decades, numerous approaches have been presented to support stakeholders in analyzing feature models. Such analyses are commonly reduced to satisfiability problems, which suffer from the growing number of options. While first attempts have been made to decompose feature models into smaller parts, they still require to compose all parts for analysis. We propose the concept of a feature-model interface that only consists of a subset of features, typically selected by experts, and hides all other features and dependencies. Based on a formalization of feature-model interfaces, we prove compositionality properties. We evaluate feature-model interfaces using a three-month history of an industrial feature model from the automotive domain with 18,616 features. Our results indicate performance benefits especially under evolution as often only parts of the feature model need to be analyzed again.

The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches, which either transform compile-time into runtime variability or make verification tools variability-aware. Existing approaches either focus on theorem proving, model checking, or other verification techniques. For the first time, we combine theorem proving and model checking to evaluate their synergies for product-line verification. We provide tool support by connecting five existing tools, namely FeatureIDE and FeatureHouse for product-line development, as well as KeY, JPF, and OpenJML for verification of Java programs. In an experiment, we found the synergy of improved effectiveness and efficiency, especially for product lines with few defects. Further, we experienced that model checking and theorem proving are more efficient and effective if the product line contains more defects.