Information Technology Reference
In-Depth Information
expressions
f
Ω
(for each mapping one expression), we use class subsumption
to get the counterparts. For this purpose, we have to iterate over each element
that is a subclass of
Required
,
Conjunct
and
Exclusive
, but without any further
classification. (ii) The second step is a further knowledge base classification, in
order to find those expressions
f
Ψ
.
Class subsumption and classification are both standard reasoning services that
are quite tractable in practice. The DL expressivity is
SHOIN
.
that are not equivalent to the top class
5 Correctness of the Validation
This section demonstrates the correct capturing of the constraints in DL by the
implication
f
Φ
⇒
f
Ω
. We start with an consideration of the constraint coverage
by these expressions. Afterwards, we show that well-formedness of the business
process model template can be concluded from the implication checking.
Constraint Coverage.
In our case, we know that both models are correct
on its own. Hence, a violation of the well-formedness constraints can only be
caused by the mappings. Our aim is to guarantee the well-formedness of each
process model from the business process model template, for each valid feature
configuration. We consider different cases how an element
E
might be involved
in a feature mapping. In case the element is not mapped, there might be no
violation, since the constraint types only contains mapped elements.
E
remains
in each process model and is not involved in any constraint with another element.
If
E
is mapped to at least one feature
F
, it depends whether
E
is involved in
a well-formedness constraint. In case
E
is not involved, there cannot be any vio-
lation of a well-formedness constraint, due to the same reasons as for unmapped
elements. More dicult is the case when
E
is involved in one of the constraints.
The constraint expression
f
Ω
(Def. 4) encodes the corresponding constraint of
E
with its counterpart elements, e.g., sibling elements. The intention of
f
Ω
is,
that the encoded constraint has to be satisfied in all business process models.
Hence, we have to check whether
f
Ω
holds for each feature configuration.
Again, we know that without any mapping there is no violation in the business
process model template. Therefore, we know that only the constraints of the
mapped feature
F
might lead to a violation of
f
Ω
. The expression
f
Φ
captures
these constraints of all mapped features
F
of
E
. We build
f
Φ
as a conjunction
on all these features (cf. Def. 4) to capture the case that there are multiple
mappings of one element
E
. The constraints of the features are directly given
by the definition of the parent features and the cross-tree constraints of
F
.
The alignment is solved by a design decision of the mapping model
(cf. Sect. 3.3). The property
feature
maps an element
E
toafeature
F
,byan
axiom
Map
E
∃
feature.F
. The property
hasF eature
is defined as a subprop-
erty of
feature
from the mapping space (Axiom 10). Hence, all class expressions
from the problem space using the property
hasF eature
are subsumed by expres-
sions where this property is replaced by its superproperty
feature
.InDef.4,we
use
Map
E
instead of elements
E
in the expression
f
Ω
. Hence,
f
Φ
and also
f
Ω
