*For the most recent entries see the
Petri Nets Newsletter.*

## Probabilistic Validation of a Remote Procedure Call Protocol.

Bennacer, N.;
Gloring, G.;
Fraize, C.;
Natkin, S.
In:
Valette, R.: *Lecture Notes in Computer Science, Vol. 815; Application and Theory of Petri Nets 1994, Proceedings 15th International Conference, Zaragoza, Spain*, pages 59-78.
Springer-Verlag,
1994.

Abstract:
Classical validation approach tries to prove that failed events (events
that do not verify an user property) will never occur. Probabilistic
validation relies on a partial analysis on a system model and tries to
prove that the failed event occurrences, have a sufficiently low
probability. An incorrect behavior is a very rare event: it is the
consequence of a complex unknown operation sequence. The system to be
validated is modeled by a stochastic Petri net. The sequence of transition
firings which may lead to critical (failed) Petri net markings are
characterized at the Petri net level. An efficient travel through the
reachability graph must be able to visit these sequences to reach as
quickly as possible critical markings. From the incidence matrix of the
net and the specification of the properties to be fulfilled, we derive a
linear system called the ``decision system''. The set of the decision
system solutions includes all characteristic vectors of sequences leading
to critical markings. In this paper, we present the probabilistic
validation of a Remote Procedure Call protocol. The goal is to evaluate
the probability that the protocol satisfies the required ``at most once''
semantic. This model is solved using two probabilistic validation
algorithms using the above principles. The first one is related to acyclic
Markov graphs. A traversal technique combining a breadth and a depth first
search traversal techniques is used considering only the critical
trajectories. The second algorithm is a worst event driven and importance
sampling simulation.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*