Information Technology Reference
In-Depth Information
Algorithm 1: Checking
EX f
1
(
1
)
check EX
(
f
1
,v
EX
){
(
2
)
for each t
z
1
nz
2
V
=
∈
T
*
{
for each
(
f
1
,V
P
)
∈
(
3
)
label
(
z
2
)
V
(
4
)
if
(
SAT-VM
(
OVM, v
EX
∧
∧
V
P
))
V
(
5
)
label
(
z
1
)
=
label
(
z
1
)
∪
(
EX f
1
;
(
v
EX
∧
∧
V
P
))
(
6
)}}}
The correctness of the presented adaption follows from the following observa-
tion. The algorithm checks each outgoing transition of each state and all possible
labels. Therefore, every possible witness for
EX f
1
will be identified.
The worst case runtime of the presented algorithm is linear in the number of tran-
sitions and labels, since every transition is considered only once by the algorithm.
For each transition, the algorithm considers each label of the destination state of the
considered transition.
5.2.3 Checking the Completeness of Witnesses
The existing single system algorithms for model checking rely on witnesses to show
that a property is fulfilled (or not fulfilled) for a given system [
3]
. This approach is
not sufficient for product lines, since a domain artifact represents a set of systems
and thus a witness must exist for every possible system. We address this challenge
by checking the completeness of witnesses for all possible systems. Algorithm 2
presents the completeness check for witnesses. The algorithm has three parameters:
the property
f
and the state
z
for which the completeness check has to be performed,
and the variant
v
which is related to the property
f
. The variant
v
is empty, if
f
is a
common property.
Algorithm 2: Checking Completeness of Witnesses
(
1
)
checkCompletness
(
f, z, v
p
){
(
2
)
if
(
SAT-VM
(
OVM, v
p
∧
(
f, V
)
∈
Label
(
z
)
¬
V
)
=
false)
(
3
)
output "There is a witness for each product";
(
4
)
else
(
5
)
output "There is at least one product without a witness";
(6)}
∧
(
The algorithm works as follows. It checks in line (2) if the orthogonal variability
model can fulfill a variant selection in which
v
p
is selected and all possible variant
selections related to the witnesses for
f
are not selected (i.e. (
∧
(
f
,
V
)
∈
Label
(
z
)
¬
V
)).
If this is not possible, it is not possible to derive a product which has no witness for
the property
f
in state
z
. If such a variant selection exists, this variant selection is an
example for a derived product that has no witness for the property
f
.
Search WWH ::
Custom Search