Promela |
Omissions |
probabilities(7) |
NAME
probabilities
-
for distinguishing between high and low probability events.
DESCRIPTION
There is no mechanism in Promela for indicating the
probability of an event.
It is possible to build a verification system that supports
event probabilities, but this comes at a price in performance,
and can have unintended side-effects. In Spin the attempt is
to build a stronger verification system by abstracting
from the probability of event sequences.
Spin is designed to check the unconditional correctness of a system. A design error in principle always has a low probability of occurrence. After all, the high probability event scenarios are easily intercepted with standard testing and debugging techniques, but only model checking techniques are able to reproducible detect the remaining classes of errors. Phrased differently: verification in Spin is concerned with possible behaviors, not with probably behaviors.
In some cases it can, nonetheless, be useful to exclude known low probability event scenarios from further consideration in a verification. Progress labels can be used to accomplish this with precise control, as explained in progress(2).
NOTES
It is possible to influence the probability that an option
in a non-deterministic selection is chosen during random
simulations, by replicating the option.
SEE ALSO
progress(2), if(2), do(2).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |