Information Technology Reference
In-Depth Information
When comparing the results of applying tests to processes, we need to compare
subsets of
. There are two standard approaches to make this comparison, based on
viewing these sets as elements of either the Hoare or Smyth powerdomain [
5
,
6
]of
O
O
.For
O
1
,
O
2
∈
P
+
(
O
), we let:
(i)
O
1
≤
Ho
O
2
if for every
o
1
∈
O
1
there exists some
o
2
∈
O
2
such that
o
1
≤
o
2
(ii)
o
2
.
Using these two comparison methods we obtain two different semantic preorders for
processes:
O
1
≤
Sm
O
2
if for every
o
2
∈
O
2
there exists some
o
1
∈
O
1
such that
o
1
≤
(i)
For
P
,
Q
∈
P
roc
, let
P
may
Q
if
A
(
T
,
P
)
≤
Ho
A
(
T
,
Q
) for every test
T
(ii)
Similarly, let
P
must
Q
if
A
(
T
,
P
)
≤
Sm
A
(
T
,
Q
) for every test
T
.
We use
P
must
Q
to denote the associated equivalences.
The terminology
may
and
must
refers to the following reformulation of the same
idea. Let
Pass
may
Q
and
P
, i.e. satisfying that
o
≥
ↆ
O
be an
upwards-closed
subset of
O
o
Pass
imply
o
∈
and
o
Pass
. It is thought of as the set of outcomes that can be
regarded as
passing
a test. Then we say that a process
P may
pass a test
T
with an
outcome in
Pass
, notation “
P
may
Pass T
”, if there is an outcome
o
∈
∈
A
(
P
,
T
) with
o
Pass
, and likewise
P must
pass a test
T
with an outcome in
Pass
, notation “
P
must
Pass T
”, if for all
o
∈
∈
A
(
P
,
T
) one has
o
∈
Pass
.Now
∈
P
↑
(
P
may
Q
iff
∀
T
∈
T
∀
Pass
O
)(
P
may
Pass T
⃒
Q
may
Pass T
)
∈
P
↑
(
P
must
Q
iff
∀
T
∈
T
∀
Pass
O
)(
P
must
Pass T
⃒
Q
must
Pass T
)
P
↑
(
where
.
Let us have a look at some typical instances of the set
O
) is the set of upwards-closed subsets of
O
O
and its associated partial
order
≤
.
1. The original theory of testing [
1
,
2
] is obtained by using as the set of outcomes
O
the two-point lattice
failure.
2. However, for probabilistic processes we consider an application of a test to a pro-
cess to succeed with a given probability. Thus we take as the set of outcomes the
unit interval [0, 1] with the standard mathematical ordering; if 0
with
representing the success of a test application, and
↥
1,
then succeeding with probability
q
is considered better than succeeding with
probability
p
. This yields two preorders for probabilistic processes which, for
convenience, we rename
≤
p<q
≤
pmay
and
pmust
, with the associated equivalences
pmay
and
pmust
, respectively. These preorders, and their associated equiva-
lences, were first defined by Wang and Larsen [
3
]. We will refer to this approach
as
scalar testing
.
Search WWH ::
Custom Search