Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les relations de transition des deux systemes a comparer, ce qui constitue une limitation en pratique. Nous proposons par consequent un algorithme original, base sur un parcours en profondeur du produit synchrone des deux systèmes, qui permet d'effectuer la comparaison ``a la volee'', sans jamais construire ni mémoriser explicitementles deux relations de transition. L'algorithme de comparaison ``a la volée'' a ete mis en œuvre au sein du logiciel de verification Aldebaran dans le cas de différentes relations : la bisimulation forte, l'équivalence observationnelle, la tau*a-bisimulation, la delay bisimulation et la bisimulation de branchement, ainsi que le preordre et l'equivalence de surete. Son application a la verification de plusieurs programmes Lotos de taille realiste a confirme l'interet pratique de notre approche par rapport aux methodes classiques. Enfin, nous nous interessons egalement a la generation d'un diagnostic lorsque les deux systemes de transitions etiquetees a comparer ne sont pas equivalents : les procedures de decision implementees dans Aldebaran fournissent le cas echeant un ensemble de sequences d'execution discriminantes, minimales pour une relation d'ordre donnee.

L'activité de test est une partie de plus en plus importante dans les développements logiciels. Cette activité de test est souvent longue et répétitive, les travaux entrepris dans cette thèse ont pour objectif de décharger l'ingénieur de test des tâches les plus répétitives de la synthèse de tests. Notre approche, dans le cadre du test de conformité, se base sur le fait qu'il existe différents niveaux d'abstraction pour définir des tests les tests exécutables pour une cible technologique, les tests abstraits qui sont indépendants de la technologie et les objectifs de test qui ne représentent que partiellement le chemin d'un test dans la spécification. Nos travaux portent sur deux points. le premier point vise à réduire l'effort alloué à la conception des tests. Pour cela nous définissons un nouveau niveau d'abstraction : les schémas de test qui offrent une abstraction supplémentaire sur les instances et valeurs manipulées. L'outil TObiAs a été développé au cours de la thèse pour aider à la conception des schémas de test, les déplier en objectifs de test ou en cas de test, puis concrétiser ces cas de test. le deuxième point étudie la portée d'un schéma de test en mesurant sa couverture de la spécification, au niveau d'abstraction du schém de test. Pour ce faire nous étudions les relations entre les niveaux d'abstraction de test et la spécification. Nous présentons l'intérêt de proposer une notion de couverture au niveau des schémas de test en construisant une abstraction de la spécification ainsi que l'outil CoPAS que nous avons créé pour calculer la couverture a priori.