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

product line (the operator AG “always globally” means that these properties must
always be fulfilled). The variability is described by the variants of the variability
model and by the relationships between the variants and the specification elements.
If one ignores the variability model and applies a model checking approach from
single system engineering to the example presented in Fig. 2, the model checking
approach would state that both defined properties are not fulfilled by the specified
system, since it is possible to reach the states ( yellow flash , closing ) and ( yellow ,
closing ) which are counterexamples for the validity of each property.
However, this verification result would be incorrect. The variability model does
not allow to derive a product from the domain artifacts for which the property
AG ( closing yellow ) is specified and which is able to reach the state ( yellow

flash , closing ), or vice versa for which the property AG ( closing

⇒

⇒ yellow flash )

is specified and which is able to reach the state ( yellow , closing ).
One way to apply model checking approaches from single-system engineering in
product line engineering would be to derive every possible product from the domain
artifacts and then verify each derived product individually. However, as it has been
discussed in Sect. 3.3, such a “brute force” approach is not feasible for product lines
of industrial size.

5 Model Checking in the Presence of Variability

In this section, we illustrate the adaptation of a model checking algorithm in order
to enable the comprehensive quality assurance of a domain artifact. The verification
of the AG operator is shown in [ 9] . In this chapter, we focus for illustration purpose
on the next-time-operator ( EX f 1 ) which can be verified easily for single system and
only requires minor adaptation for the verification of domain artifacts. The next-
time-operator, EX f 1 evaluates to true, if there is one path starting at the initial state
on which f 1 holds on the next state.
The presented approach is based on the model checking approach from Clarke
et al. [ 2] which is considered as one of the fundamental approaches for model check-
ing. The main idea of the approach is to include the variability information specified
in the variability model (as Boolean variables) in the model checking algorithms.
During the exploration of the state space, the algorithms consider the variabil-
ity model to ensure that the current path explored in the state space is valid with
respect to the variability model. Algorithms for the verification of other properties
are presented in [ 10] .

5.1 Formal Foundations

In this section, we give a brief introduction into the formal foundations of our
approach. To reason about the variability model of a product line, the variability
model is formalized as follows: