Information Technology Reference
In-Depth Information
Chapter 4
Probabilistic Testing Semantics
Abstract
In this chapter we extend the traditional testing theory of De Nicola and
Hennessy to the probabilistic setting. We first set up a general testing framework,
and then introduce a vector-based testing approach that employs multiple success
actions. It turns out that for finitary systems, i.e. finite-state and finitely branching
systems, vector-based testing is equivalent to scalar testing that uses only one success
action. Other variants, such as reward testing and extremal reward testing, are also
discussed. They all coincide with vector-based testing as far as finitary systems are
concerned.
·
·
·
Keywords
Testing semantics
Vector-based testing
Scalar testing
Reward testing
4.1
A General Testing Framework
It is natural to view the semantics of processes as being determined by their ability to
pass tests [
1
-
4
]; processes
P
1
and
P
2
are deemed to be semantically equivalent unless
there is a test that can distinguish them. The actual tests used typically represent the
ways in which users, or indeed other processes, can interact with
P
i
.
Let us first set up a general testing scenario within which this idea can be
formulated. It assumes:
•
a set of processes
P
roc
•
a set of tests
T
, which can be applied to processes
•
a set of outcomes
O
, the possible results from applying a test to a process
ₒ
P
+
(
•
a function
A
:
T
×
P
roc
O
), representing the possible results of applying
a specific test to a specific process.
P
+
(
Here
O
) denotes the collection of nonempty subsets of
O
; so the result of
applying a test
T
to a process
P
,
(
T
,
P
), is in general a
nonempty set
of out-
comes, representing the fact that the behaviour of processes, and indeed tests, may
be nondeterministic.
Moreover, some outcomes are considered better then others; for example, the
application of a test may simply succeed, or it may fail, with success being better
than failure. So we can assume that
A
O
is endowed with a partial order, in which
o
1
≤
o
2
means that
o
2
is a better outcome than
o
1
.
Search WWH ::
Custom Search