Abstract FR:

Les techniques de description formelle (tdf) pour la specification de systemes communicants sont utilisees pour valider et tester des implementations de ces systemes. Dans le cas de systemes constitues de modules, il est interessant de savoir evaluer la testabilite de chacun des composants a travers l'environnement de test que constitue les autres composants interconnectes. Cette these presente deux contributions principales aux approches de validation et de test dans le cadre des tdf: 1) une caracterisation operationnelle des relations de conformite, avec derivation automatique de tests de conformite; 2) une approche d'analyse de la testabilite des systemes partiellement observables et commandables. Les deux contributions sont basees sur une structure de graphe doublement etiquete: le graphe de refus. La verification automatique de conformite est basee sur un calcul de bissimulation adapte a cette structure. L'analyse de testabilite est basee sur l'ordonnancement de modeles d'implementations erronees. La definition des operateurs de composition et restriction sur les graphes de refus permet d'ameliorer l'efficacite de la recherche des limites de testabilite. Un environnement logiciel a ete developpe sous environnement unix pour (1) la verification des relations de conformite dans le cas des systemes a etats finis; 2) la generation de tests de conformite, et pour; 3) la mise en uvre de l'analyse de testabilite d'un systeme a travers un environnement