Information Technology Reference
In-Depth Information
•
Each variant of the variability model is represented as a Boolean variable
v
i
,
which evaluates to
true
if the corresponding variant is included in the derived
product under consideration.
•
The set of all such Boolean variables of an OVM is called
V
.
•
The constraints of the variability model are formalized by a Boolean expres-
sion OVM(
v
) over the variables in
V
.OVM(
v
) evaluates to
true
for each valid
product of the software product line, i.e., OVM(
v
) only evaluates to
true
,ifthe
variants included in the derived product under consideration satisfy all variability
dependencies and all constraint dependencies.
For more details on the formal specification of the orthogonal variability model, we
refer to [
17]
.
For the specification of the behavior of the products of the product line, we
use I/O-automata which are an established language for modeling concurrent and
distributed discrete event systems [
13]
and are also used for specifying domain arti-
facts [
7]
. The specification of a system typically consists of a set of I/O-automata
C
,
C
n
}. An I/O-automaton
C
i
is defined as 5-tuple (
Z
i
,
z
0
,i
,
Send
i
,
Receive
i
,
T
i
) where
=
{
C
1
,
...
•
Z
i
is the set of states,
•
z
0
,i
∈
Z
i
is the initial state,
•
Send
i
is the set of sendable messages,
•
Receive
i
is the set of receivable messages (
Send
i
∩
Receive
i
=
Ø),
•
T
i
⊆
Z
i
×
×
=
Send
i
∪
M
Z
i
;(
M
Receive
i
) is the transition relation.
For documenting variability in I/O-automata, we define a variability relationship
between the transitions
T
i
of the I/O-automaton and the variants
V
of the variability
model as follows:
VRel
IO
⊆
V
× P
(
v,T
)
T
,
•
t
∈
T
i
is variable, if
t
is related to a variant:
∃
∈
VRel
IO
:
t
∈
(
v,T
)
T
.
•
t
∈
T
i
is common, if
t
is not related to a variant:
∀
∈
VRel
IO
:
t
∈
Without loss of generality, we assume that a transition cannot be related to more
than one variant, i.e.
(
v
1
,
T
1
), (
v
2
,
T
2
)
VRel
IO
:(
T
1
∩
T
2
=
v
2
), since
every orthogonal variability model with multiple artifact dependencies between
variants and artifacts can be transformed into an orthogonal variability model with
a unique artifact dependency. A proof of this claim can be found in [
8]
.
In order to perform the verification of a set of automata, the set of automata
is integrated into one automaton by a product construction [
14]
. Existing single
system algorithms for the product construction do not incorporate the variability of
the product line. We refer to
[10]
for a description of an algorithm that incorporates
∀
∈
Ø)
∨
(
v
1
=
1
P
(T
i
) denotes the power set of T
i
.
Search WWH ::
Custom Search