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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Ajmone-Marsan, G. Balbo, G. Chiola, G. Conte and A. Cumani. On Petri nets with stochastic timing. PNPM85, IEE CN 85CH2 187-3, Turin, July, 1985.
J. Barancourt. Modélisation et validation d'un protocole de RPC. Rapport de stage de DEA de systèmes informatiques, Université de Paris VI, 1991.
N. Bennacer and G. Florin S. Natkin. Probabilistic validation using worst event driven and importance sampling simulation. CEDRIC Report 93-14 submitted to the 13th symposium on Reliable Distributed Systems, October, 1994.
K. Barkaoui G. Florin C. Fraize B. Lemaire S. Natkin. Reliability analysis of non repairable systems using stochastic Petri nets. 18th Symposium on Fault Tolerant and Computing Systems, Tokyo, June 1988.
A. R. Cavalli and E. Paul. Exhaustive analysis and simulation for distributed systems, both sides of the same coin. Distributed computing, n 2, 1988.
E. Cinlar. Introduction to stochastic processes. Prentice Hall 1975.
A. E. Conway and A. Goyal. Monte Carlo simulation of computer system availability/reliability models. Proceeding of the seventeenth symposium on Fault Tolerant Computing vol 6, pp 230–235, 1987.
Chorus distributed operating systems C. Delorme. Spécifications de l'IPC Chorus V3.3, documentation interne, CS/TN-89-18, February, 1990.
G. Florin C. Fraize S. Natkin. Stochastic Petri nets: properties, applications and tools. Micro-electronics and reliability, vol 31, n 4, pp 669–698, 1991.
G. Florin C. Fraize S. Natkin. A new approach of formal proof: probabilistic validation. International working conference on Dependable Computing for Critical Applications, Tucson, Arizona, pp 18–20, February, 1991.
G. Florin C. Fraize S. Natkin. Searching best paths to worst states. International working conference on Petri Nets Performance Models, Melbourne, pp 204–209, December, 1991.
C. Fraize. Validation Probabiliste des systèmes sécuritaires ou distribués modélisés en termes de réseaux de Petri Stochastiques. Thèse de Doctorat, CNAM Paris, February, 1993.
P. W. Glynn D. L. Iglehart. Importance Sampling for stochastic simulations. Management Science, vol 35, n 11, November, 1989.
J. Gorski. Design for safety using temporal logic. Safecomp, Sarlat, France, 1986.
B. T. Halpern and S. Oowicki. Modular verification of computer communication protocols. IEEE transactions on communications, vol com-31. n 1, 1983.
J. P. Haas and G. S. Shedler. Modelling power of stochastic Petri nets for simulation. Probability in the engineering and information sciences, n 2, pp 135–159, 1988.
E. E. Lewis F. Böhm. Monte Carlo simulation of Markov unreliability models. Nuclear Engineering and Design, vol 77, pp 49–62, 1984.
V. F. Nicola M. K. Nakayama P. Heidelberger A. Goyal. Fast simulation of dependability models with general failure, repair and maintenance processes. Proceedings of the twentieth symposium on fault-tolerant computing, pp 491–498, June, 1990.
J. P. C. Kleijnen. Statistical Techniques in simulation. Part 1 Marcel Dekker, 1974.
M. Silva. Structural analysis of Petri nets. Tutorials PNPM93, Toulouse, October, 1993.
A. Tanenbaum. Communication networks. Second edition. Prentice-Hall editions.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bennacer, N., Florin, G., Fraize, C., Natkin, S. (1994). Probabilistic validation of a Remote Procedure Call protocol. In: Valette, R. (eds) Application and Theory of Petri Nets 1994. ICATPN 1994. Lecture Notes in Computer Science, vol 815. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58152-9_5
Download citation
DOI: https://doi.org/10.1007/3-540-58152-9_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58152-9
Online ISBN: 978-3-540-48462-2
eBook Packages: Springer Book Archive