Information Technology Reference
In-Depth Information
the variability. The result of this algorithm is an extended transition relation that
captures the combined behavior of the integrated automata. The extended transition
(named as
T
∗
) combines a transition with the variant selection information (
V
) that
is necessary to select a particular transition for a product and is defined as follows:
T
∗
⊆
V
.
Z
×
(
Send
∪
Receive
)
×
Z
×
5.2 Adaptation of Model Checking for EX f
5.2.1 Adaption of State Labeling
The model checking approach from Clarke et al. [
2]
labels each state with the prop-
erties that are fulfilled in this state. In variable I/O-automata, the fulfillment of a
property may rely on variable transitions. Therefore, the state labeling may include
the variant selection which is necessary to fulfill the property. To incorporate the
variability, we extend the labeling procedures introduced by Clarke et al.
[2]
as fol-
lows: Let
f
be a CTL expression, let
z
Z
be a state of an I/O-automaton, and let
V
be a (possibly empty) selection of variants. The state
z
is labeled with (
f
,
V
) (i.e.
(
f
,
V
)
∈
label
(
z
)), if
f
1
is fulfilled in state
z
for the selection
V
of variants.
∈
5.2.2 Adaption of the Verification Algorithm
For the property
EX f
1
, every state should be labeled with
EX f
1
which has some suc-
cessor state that is labeled with
f
1
. Since the transitions in a variable I/O-automaton
and the property
f
1
can be variable, it is necessary to check whether the variants
related to
f
1
, to the considered transition, and to
EX f
1
can be selected together.
Algorithm 1 shows the calculation of the expression
EX f
1
for a variable I/O-
automaton. The algorithm has two parameters: first, the property
f
1
which should
be checked and, second, the variant
v
EX
which is related to
EX f
1
. The variant
v
EX
is
empty, if
f
1
is a common property.
For each outgoing transition of each state of a variable I/O-automaton, the
algorithm checks the following. If the reached state
z
2
is labeled with
f
1
and the
combined selection of variants of the property (i.e.
v
EX
), the selection variants of
the current transition (i.e.
V
), and the selection of variants associated with
f
1
in the
V
∧
V
P
)) (line (5) and (6)). This label documents that
EX f
1
is fulfilled if the vari-
ants documented by (
v
EX
∧
V
∧
V
P
) are selected. If the start state
z
0
is labeled, a
witness for
EX f
1
has been identified.
2
The function
SAT-VM
(
OVM, V
) checks whether there is a selection of variants that fulfils the
variability
OVM
and the selection of variants
V
.
Search WWH ::
Custom Search