Abstract FR:

Le but de cette these est de fournir de nouvelles idees aux concepteurs d'outils de validation. Traitant du probleme indecidable de la finitude des graphes d'accessibilite de modeles de specification autorisant des files fifo, nous donnons une condition suffisante fondee sur une relation entre etats accessibles. Cette relation fournit un test pouvant s'appliquer a toutes les specifications du modele et meme aux programmes estelle. En depit de cette approche, nous ameliorons les resultats theoriques connus. Une des limitations principales des outils de validation est l'exposition du graphe d'etats. Mais certaines proprietes peuvent etre verifiees au cours d'un parcours du graphe d'accessibilite. Nous experimentons donc un parcours en profondeur avec remplacement aleatoire qui peut augmenter de facon significative la taille des graphes analysables. Nous discutons ensuite de l'utilisation du parcours avec remplacement pour la verification a la volee. Nous donnons en particulier un algorithme original et efficace permettant la verification d'une specification par un automate de buchi. Finalement, nous donnons quelques idees pour la construction d'un outil de validation incorporant le parcours avec remplacement