Information Technology Reference
In-Depth Information
to by the server, and let
a
represent the activity of the server (0 for
polling and 1 for serving). The property can then be expressed as the formula
P
≥
0
.
4
[
∈{
0
,
1
}
a
=1]. We verify this formula in the state where the
server is about to attend to station 1 (
s
=1 and
a
=0) and all buffers are empty.
If both station 1 and station 2 fail before they are served,
¬
(
s
=2
∧
a
=1)
U
s
=1
∧
¬
(
s
=2
∧
a
=1) will
remain true and
s
=1
a
=1 false indefinitely, and a sample trajectory for the
given model-checking problem may never terminate.
We have implemented the two sampling-based algorithms described in this pa-
per in
∧
[24]. We compare the sampling-based approaches with numerical
iterative algorithms implemented in
Ymer
[17]. For the experiments, we used
α
=
β
=0
.
01 and
δ
=0
.
005 for the sampling-based algorithms, and
=0
.
005
(absolute error) for the numerical algorithms. These choices are of course some-
what arbitrary. Younes and Simmons [26] provide a thorough investigation of
how these parameter choices affect performance for sampling-based algorithms.
For example, using
α
=
β
=10
−
8
increases verification time by about a factor
10. For the reachability approach, we tried both Wald's SPRT [23] (sequential
hypothesis testing) and estimation based on the Hoeffding bound [15] that gives
afixedsamplesizeof
N
=
PRISM
2
δ
2
log
α
1
(105,967 for our choice of parameters). For
the approach based on termination probability we used Chow and Robbins' se-
quential estimation procedure mentioned earlier and
p
T
=10
−
4
(this choice was
made after computing the subdominant eigenvalue for the transition matrices of
models with up to 12 stations). Finally, for the numerical approaches, we used
thehybridenginein
, trying both Jacobi and (backwards) Gauss-Seidel.
Figure 3 plots the verification time as a function of state-space size for the
modified polling system, when verifying the stated property using different al-
gorithms. For the sampling-based approaches, the graph shows the average time
over 20 trials. The state-space size for a model with
n
stations is 4
n
PRISM
3
n−
1
.A
·
model with 24 stations, for example, has close to 10
13
states.
The sampling-based approaches scale well as the state-space size grows. Reach-
ability combined with the SPRT does best, partly because the underlying prob-
ability is close to 0
.
5, while the bound in the formula is 0
.
4, so a decision can
be reached with an average sample size of about 1,200. The estimation-based
approaches require much larger sample sizes. The termination-based approach
beats the reachability-based approach when the latter is used with a sample size
derived from the Hoeffding bound.
The numerical algorithms are much faster for small state spaces, but perfor-
mance deteriorates quickly for larger state spaces. They also use more memory
than the sampling-based approaches. For a model with 16 stations (about 1
billion states),
caused serious thrashing on a computer equipped with
8 GB of RAM. The reachability-based approach has a much more modest mem-
ory growth, and nothing suggests that it could not handle models much larger
than what we have tested here. The termination-based approach uses the least
amount of memory, as it does not require reachability analysis, and does not show
any noticeable growth as models get bigger. The sampling-based approaches are
trivially parallelizable, so we could get a speedup on multi-core architectures.
PRISM
Search WWH ::
Custom Search