Probabilistic validation of a Remote Procedure Call protocol

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.