Abstract FR:

La validation de systemes informatiques complexes et en particulier de systemes securitaires ou distribues est indispensable dans une optique de surete de fonctionnement de ces systemes. Les approches reposant sur une analyse exhaustive se heurtent rapidement au caractere combinatoire du probleme. Les techniques basees sur la simulation des specifications sont plus aisees a appliquer, mais ne constituent pas une preuve. Le but de notre travail est de developper une nouvelle technique de validation: la validation probabiliste. L'approche repose sur une description precise du comportement temporel du systeme et a pour objectif de demontrer que des assertions de bon fonctionnement definies sur un modele sont verifiees, durant la vie operationnelle du systeme, avec un seuil de probabilite suffisant. Le systeme a valider est modelise par un reseau de petri stochastique. L'analyse repose sur une exploration partielle du graphe des marquages accessibles. Cette approche tend a atteindre le plus rapidement possible des etats ne verifiant pas les assertions de bon fonctionnement specifiees. Dans chaque marquage, un systeme de decision (en fait un programme lineaire) permet de selectionner les transitions susceptibles de conduire a de tels etats, guidant ainsi l'exploration du graphe. L'exploration s'arrete lorsqu'une precision suffisante sur les probabilites d'atteinte est obtenue. Deux algorithmes bases sur ces principes ont ete developpes et appliques a la validation probabiliste du protocole d'appel de procedure distante du systeme d'exploitation reparti chorus. L'assertion de bon fonctionnement specifiee est le respect de la semantique au plus une fois (une requete d'un client est traitee au plus une fois par le serveur). Nous montrons qu'il n'est possible de garantir cette semantique qu'avec une certaine probabilite, liee notamment a l'incertitude des delais de transmission des messages