Les travaux de cette thèse s'inscrivent dans le cadre de la vérification des logiciels et plus particulièrement du test à partir de spécifications algébriques. La soumission d'un jeu de tests exhaustif pour trouver toutes les erreurs d'un programme est généralement impossible. Il faut donc sélectionner un jeu de tests le plus judicieusement possible. Nous avons donc donné une méthode de sélection de tests par dépliage des axiomes de spécifications conditionnelles positives (clauses de Horn pour la logique équationnelle). Celle-ci permet de partitionner le jeu exhaustif des tests. Nous utilisons pour cela un critère de sélection qui utilise les axiomes de la spécification et qui peut être appliqué plusieurs fois de suite. Pour garantir de bonnes propriétés sur ce critère de sélection, nous avons également donné un cadre général pour la normalisation d'arbre de preuve. Il fonctionne pour n'importe quel système formel, et permet d'unifier un grand nombre de résultats en logique.

Le test est l'une des méthodes les plus utilisées pour la validation du logiciel. L'activité de test consiste à exécuter le logiciel sur un sous-ensemble de ses entrées possibles de manière à déceler d'éventuelles erreurs. La présence d'erreurs est établie par confrontation du comportement du logiciel avec un objet de référence. Le processus de test est généralement décomposé en trois phases : la sélection du sous-ensemble des entrées sur lequel le logiciel sera exécuté, la soumission de ces entrées au logiciel en collectant les sorties (les réponses du logiciel) et la décision de l'adéquation de ces sorties avec les sorties attendues.<br /><br />La sélection des données à soumettre au logiciel peut être effectuée selon différentes approches. Lorsque la phase de sélection d'un jeu de tests est opérée à partir d'un objet de référence décrivant plus ou moins formellement le comportement du logiciel, sans connaissance de l'implantation elle-même, on parle de test « boîte noire ». Une des approches de test boîte noire pour laquelle un cadre formel a été proposé est celle qui utilise comme objet de référence une spécification logique du système sous test.<br /><br />Le cadre général de test à partir de spécifications logiques (ou axiomatiques) pose les conditions et les hypothèses sous lesquelles il est possible de tester un système. La première hypothèse consiste à considérer le système sous test comme un modèle formel implantant les opérations dont le comportement est décrit par la spécification. La seconde hypothèse a trait à l'observabilité du système sous test. Il faut fixer la forme des formules qui peuvent être interprétées par le système, c'est-à-dire qui peuvent être des tests. On se restreint généralement au moins aux formules qui ne contiennent pas de variables. Une fois ces hypothèses de test posées, on dispose d'un jeu de tests initial, celui de toutes les formules observables qui sont des conséquences logiques de la spécification. <br /><br />Le premier résultat à établir est l'exhaustivité de cet ensemble, c'est-à-dire sa capacité à prouver la correction du système s'il pouvait être soumis dans son intégralité. Le jeu de tests exhaustif étant le plus souvent infini, une phase de sélection intervient afin de choisir un jeu de tests de taille finie et raisonnable à soumettre au système. Plusieurs approches sont possibles. L'approche suivie dans ma thèse, dite par partition, consiste a diviser le jeu de tests exhaustif initial en sous-jeux de tests, selon un certain critère de sélection relatif à une fonctionnalité ou à une caractéristique du système que l'on veut tester. Une fois cette partition suffisamment fine, il suffit de choisir un cas de test dans chaque sous-jeu de test obtenu en appliquant l'hypothèse d'uniformité (tous les cas de test d'un jeu de test sont équivalents pour faire échouer le système). Le deuxième résultat à établir est que la division du jeu de tests initial n'ajoute pas (correction de la procédure) et ne fait pas perdre (complétude) de cas de test.<br /><br />Dans le cadre des spécifications algébriques, une des méthodes de partition du jeu de tests exhaustif qui a été très étudiée, appelée dépliage des axiomes, consiste à procéder à une analyse par cas de la spécification. Jusqu'à présent, cette méthode s'appuyait sur des spécifications équationnelles dont les axiomes avaient la caractéristique d'être conditionnels positifs (une conjonction d'équations implique une équation).<br /><br />Le travail de ma thèse a eu pour but d'étendre et d'adapter ce cadre de sélection de tests à des systèmes dynamiques spécifiés dans un formalisme axiomatique, la logique modale du premier ordre. La première étape a consisté à généraliser la méthode de sélection définie pour des spécifications équationnelles conditionnelles positives aux spécifications du premier ordre. Ce cadre de test a ensuite été d'adapté à des spécifications modales du premier ordre. Le premier formalisme de spécification considéré est une extension modale de la logique conditionnelle positive pour laquelle le cadre de test a été initialement défini. Une fois le cadre de test adapté aux spécifications modales conditionnelles positives, la généralisation aux spécifications modales du premier ordre a pu être effectuée. <br /><br />Dans chacun de ces formalismes nous avons effectué deux tâches. Nous avons d'une part étudié les conditions nécessaires à imposer à la spécification et au système sous test pour obtenir l'exhaustivité du jeu de tests initial. Nous avons d'autre part adapté et étendu la procédure de sélection par dépliage des axiomes à ces formalismes et montré sa correction et sa complétude. Dans les deux cadres généraux des spécifications du premier ordre et des spécifications modales du premier ordre, nous avons montré que les conditions nécessaires à l'exhausitivité du jeu de test visé étaient mineures car faciles à assurer dans la pratique, ce qui assure une généralisation satisfaisante de la sélection dans ce cadre.