Information Technology Reference
In-Depth Information
only contain classes of the feature model and
hasF eature
and
feature
are in
a subproperty relation. The expression
f
Ω
is composed of the mapped elements
(
Map
E
of
Σ
M
) according to the logical meaning of their constraint classification
(
Required
,
Conjunct
or
Exclude
).
Formula Representation in DL.
In the validation, we check whether
f
Ψ
(
f
Ψ
≡¬
f
Φ
f
Ω
) is equivalent with
, which means to test whether the subsump-
tion
f
Φ
f
Ω
holds for each interpretation (tautology). Due to the alignment,
we can compare
f
Φ
and
f
Ω
by DL reasoning. Finally, we have to demonstrate
that this subsumption ensures that the solution space constraints are satisfied
for each allowed feature configuration (Lemma 1).
Lemma 1 (Correctness of the Validation).
For mappings from an element
E
to a set of features
F
,
f
Φ
are the constraints of
F
and
f
Ω
the constraints of
E
.If
f
Φ
is subsumed by
f
Ω
then the well-formedness constraints of all elements
E
hold.
Proof.
Looking to the different types of constraints in both spaces, we basically
deal with
implication
,
and
,
or
and
xor
. Hence, we have to consider all possible
combinations in both spaces and check whether
f
Φ
⇒
f
Ω
is a tautology. This
kind of logical problem is in the nature of propositional logic. Hence in Def. 4, we
define the DL expressions
f
Φ
and
f
Ω
in a propositional style. The term connec-
tors are the DL counterparts, e.g., the
intersection
(
) for an
and
(
∧
). Instead of
propositional variables, there are class expressions like
hasF eature.F
contain-
ing features and the properties
feature
and
hasF eature
from
Σ
Φ
and
Σ
M
.Itis
easy to see in Def. 4 that
f
Ω
is built as a DL expression representing either a con-
junctive, exclusive or implicative combination. In
f
Φ
, we conjunctively connect
the parent features and the cross-tree constraints that are already represented
in this modeling style.
∃
6 Proof-of-Concept and Discussion
The evaluation of our approach has been conducted by providing a proof-of-
concept which has been developed by integrating the FeatureMapper [10] and
the transformation of the control flow parts of BPMN to DL, as described in [11].
Setting.
We applied the validation to the case study that was introduced in
Sect. 2 and is part of the
e-store
SPL [4]. The feature model consists of 287 fea-
tures, 2 top features, 192 of the features are leaf features and all others are parent
features. There are 21 cross-tree references, including mandatory and optional
as well as OR-grouped features. The process model contains 84 activities.
In the settings, we validated feature models with 154 features and with the
entire feature model (287 features). In both cases, we build either 22 or 48
mappings. The average validation time using the Pellet reasoner is 2970 ms for
154 features with 22 mappings and 4430 ms for 287 features with 48 mappings.
The time for the transformation to DL is less that the validation time. This is
based on the fact that we use the DL-oriented feature model of [6] and we only
transform the relevant control flow informations of BPMN to DL.
