Abstract FR:

La validation probabiliste par simulation guidee a evenements rares est une nouvelle approche de validation de systemes complexes, surs de fonctionnement, securitaires et distribues. Elle repose sur une analyse partielle d'un modele du systeme et tente de prouver que la non verification de proprietes de bon fonctionnement, sur une duree d'utilisation donnee, a une probabilite suffisamment faible. Un comportement incorrect (du point de vue des proprietes requises) est un evenement rare dans la vie de ces systemes. Lorsqu'il se produit il est la consequence d'un enchainement d'evenements complexes, inconnus et par consequent difficiles a apprehender. Le systeme a valider est modelise par un reseau de petri stochastique. Une simulation efficace du reseau de petri doit etre capable d'echantillonner des trajectoires (sequences de franchissement) complexes et improbables menant aux marquages d'echec (pour lesquels la propriete a valider n'est pas verifiee). Par consequent deux problemes se posent: dans le premier probleme les sequences de tir des transitions susceptibles de conduire a l'echec (sequences critiques) doivent etre caracterisees a partir d'une analyse structurelle et qualitative du reseau de petri. De la matrice d'incidence du reseau et des specifications des proprietes a verifier, on etablit un systeme d'equations lineaires appele systeme de decision. L'ensemble des solutions de ce systeme comprend tous les vecteurs caracteristiques des sequences critiques. Le second probleme est d'augmenter la probabilite de ces sequences de facon a les parcourir avec une frequence suffisante au cours de l'echantillonnage par simulation. Une methode d'echantillonnage preferentiel est utilisee pour accroitre cette probabilite et pour construire un estimateur correct du niveau de la validation realisee. Un algorithme de simulation est developpe et implemente. Il utilise des procedures qualitatives basees sur differentes strategies de guidage et des procedures quantitatives d'echantillonnage selon differentes approches. Nous montrons l'efficacite de la validation probabiliste par les techniques developpees sur deux applications industrielles