Quality Assurance in the Presence of Variability - Intentional Perspectives on Information Systems Engineering - page 320

products. One possible approach is to avoid a separate derivation and checking of
each product, since checking each product would lead to a large number of redun-
dant checks. Instead, a comprehensive approach should directly check the domain
artifacts by taking the variability of the domain artifacts into account. However, the
challenge of this approach is to show that every possible product is checked.
In the following section, we present such a comprehensive quality assurance
approach that is based on model checking techniques and allows for a comprehen-
sive verification of domain artifacts against temporal logic properties.
4 Towards a Comprehensive Quality Assurance
in the Presence of Variability
Automated verification approaches are a common way to address quality assur-
ance in product line engineering [ 29] . Model checking [ 2] is a technique for
comprehensive quality assurance that facilitates the verification of properties
(typically specified in temporal logic, e.g. CTL) of a system (typically specified in
a state transition model). In software engineering for single-systems, model check-
ing is an established technique for verifying development artifacts in requirements
engineering, design, realization, and test [6] in different domains.
Since product line engineering addresses a set of similar products instead of a
single product, model checking of domain artifacts in product line engineering has
to be defined as follows:
Model checking of domain artifacts means to verify that every possible product that can be
derived from a domain artifact fulfills the specified properties [ 10] .
In contrast to model checking in single-system development, where a single product
is verified against expected properties, model checking in product line engineering
has to verify that a whole set of products fulfills the properties specified for each
product.
Numerous model checking approaches have been proposed for the verification
of single-system specifications [ 1, 2, 5] . However, model checking approaches from
single-system engineering cannot directly be used for the verification of domain
artifacts, since they do not consider the variability defined for the product line [ 9] .
We will illustrate this using a simple example.
Figure 2 depicts a simplified example for defining domain artifacts, properties,
and the variability of a product line [ 10] . The example depicts a simplified orthogo-
nal variability model, two I/O-automata and two properties (see [ 10] for a detailed
introduction into the modeling language). The example specifies a simple product
line for rail crossing gates which consists of a traffic light and a gate. The traffic
light exhibits alternative variable behavior: The traffic light can either show a flash-
ing yellow light or a steady yellow light when the gate is closing. The behavior can
be verified with respect to the two variable properties that specify invariants of the