Nous nous proposons de développer une méthode d'assistance à la sélection de jeux de tests à partir de spécifications formelles. Nos objectifs étant de déboucher sur une méthode de tests qui soit générale, c'est à dire qui ne soit pas dépendante d'un type de spécification formelle particulier. La méthode de tests qui nous intéresse est de type fonctionnel, ou "boîte noire", par opposition aux méthodes classiques de type structurel, ou "boîte blanche". Il s'agit d'évaluer les fonctionnalités d'un programme, sans analyser les détails de son code, mais en confrontant les résultats obtenus par l'exécution de ce code à la spécification formelle de l'application. Contrairement au code d'un programme, sa spécification formelle n'a pas pour vocation d'être exécutée, mais de décrire les comportements de l'application à l'aide de formules exprimées dans un langage logique spécialisé. La sélection d'un jeu de tests judicieux pour chaque formule permet de couvrir toutes les fonctionnalités attendues du système, et en particulier de tester les comportements critiques.