Model Checking of Domain Artifacts in Product Line Engineering

In product line engineering individual products are derived from the domain artifacts of the product line. The reuse of the domain artifacts is constraint by the product line variability. Since domain artifacts are reused in several products, product line engineering benefits from the verification of domain artifacts. For verifying development artifacts, model checking is a well-established technique in single system development. However, existing model checking approaches do not incorporate the product line variability and are hence of limited use for verifying domain artifacts. In this paper we present an extended model checking approach which takes the product line variability into account when verifying domain artifacts. Our approach is thus able to verify that every permissible product (specified with I/O-automata) which can be derived from the product line fulfills the specified properties (specified with CTL). Moreover, we use two examples to validate the applicability of our approach and report on the preliminary validation results.