Abstract
This paper presents a new concept of validation of distributed or safety-critical systems. The main problem of existing methods is related to the exponential growth of the analysis complexity with the model size. Our method relies on a state transition model which includes a description of operation duration and frequency of events (stochastic Petri nets). The aim of our work is to develop a new approach based on a partial exploration of the reachability set. At the end of the partial exploration we can demonstrate, for a given period of operation, that assertions about the behaviour of the system are verified with an acceptable probability level.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
B. Halpern and S. Owicki, “Modular verification of computer communication protocols,” IEEE Transactions on Communications, vol. com-31, no. 1, 1983. 1983.
J. Gorski, “Design for safety using temporal logic,” in Safecomp, (France), 1986.
A. Cavalli and F. Horn, “Proof of specification properties by using finite state machines and temporal logic,” in IFIP, 1987.
A. Cavalli and E. Paul, “Exhaustive analysis and simulation for distributed systems, both sides of the same coin,” Distributed Computing, vol. N2, 1988.
F. Christian, “Understanding fault-tolerant distributed systems,” Research Report RJ 6980(66517), IBM Research Division, 1990.
G. Juanole and J. Roux, “On the pertinence of the extended time petri net model for analyzing communication activities,” in PNPM, 1989.
K. Barkaoui, G. Florin, C. Fraize, B. Lemaire, and S. Natkin, “Reliability analysis of non repairable systems using stochastic petri nets,” in FTCS, June 1988.
J. Meyer and W. Sanders, “Performability evaluation of distributed systems using stochastic activity networks,” in International workshop on Petri nets and performance models, August 1987.
N. F. Maxemchuck and K. Sabnani, “Probabilistic verification of communication protocol,” Distributed Computing, vol. N3, 1989.
M. Fisher, N. Lynch, and M. Paterson, “Impossibility of distributed consensus with one faulty process,” JACM, vol. 32, 1985.
G. Florin and S. Natkin, “RDPS: a software package for the evaluation and the validation of dependable computer systems,” in Safecomp, (France), 1986.
G. Florin, C. Fraize, and S. Natkin, “Petri nets: properties applications and tools,” Microelectronic and Reliability, 1990. also Cedric Research Report.
G. Florin and S. Natkin, Les reseaux de Petri stochastiques; theorie, techniques de calcul, applications. PhD thesis, Universite de Paris VI, Paris, June 1985.
T. Murata, “Petri nets: properties, analysis and applications,” in [itProceedings of the IEEE, 1989.
E. Audureau, P. Enjalbert, and L. Farinas Del Cerro, Logique temporelle, Semantique et validation de programmes paralleles. Masson, 1990.
C. Fraize, “Les reseaux de petri stochastiques a graphes de marquages sans circuit: theorie et application a l’analyse de la fiabilite et des performances des systemes informatiques,” memoire d’ingenieur, CNAM, 1988.
M. Bouissou, “Automatic generation and quantification of event sequences leading to repairable system failure,” tech. rep., EDF — Bulletin de la Direction des Etudes et Recherches, 1987.
A. Conway and A. Goyal, “Monte carlo simulation of computer system availability reliability models,” in Proc.17th IEEE International symposium on fault tolerant computing, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1992 Springer-Verlag/Wien
About this paper
Cite this paper
Florin, G., Fraize, C., Natkin, S. (1992). A New Approach of Formal Proof: Probabilistic Validation. In: Meyer, J.F., Schlichting, R.D. (eds) Dependable Computing for Critical Applications 2. Dependable Computing and Fault-Tolerant Systems, vol 6. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9198-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-7091-9198-9_17
Publisher Name: Springer, Vienna
Print ISBN: 978-3-7091-9200-9
Online ISBN: 978-3-7091-9198-9
eBook Packages: Springer Book Archive