Abstract: La complexité croissante des systèmes réactifs fait que le test devient une technique de plus en plus importante dans le développement de tels systèmes. Un grand intérêt est notamment accordé au test de conformité qui consiste à vérier si les comportements d'un système sous test sont corrects par rapport à sa spécication. Au cours des dernières années, les théories et outils de test de conformité pour la génération automatique de test se sont développés. Dans ces théories et algorithmes, les spécications des systèmes réactifs sont souvent modélisées par différentes variantes des systèmes de transitions. Cependant, ces théories et outils ne prennent pas explicitement en compte les données du système puisque le modèle sous-jacent de système
de transitions ne permet pas de le faire. Ceci oblige à énumérer les valeurs des données avant de construire le modèle de système de transitions d'un système, ce qui peut provoquer le problème de l'explosion de l'espace d'états. Cette énumération a également pour effet d'obtenir des cas de test où toutes les données sont instanciées. Or, cela contredit la pratique industrielle où les cas de test sont de vrais programmes avec des variables et des paramètres. La génération de tels
cas de test exige de nouveaux modèles et techniques. Dans cette thèse, nous atteignons deux objectifs. D'une part, nous introduisons un modèle appelé système symbolique de transitions à entrée/sortie qui inclut explicitement toutes les données d'un système réactif. D'autre part, nous proposons et implémentons une nouvelle technique de génération de test qui traite symboliquement les données d'un système en combinant l'approche de génération de test proposée auparavant par notre groupe de recherche avec des techniques d'interprétation abstraite. Les cas de test générés automatiquement par notre technique satisfont des propriétés de correction: ils émettent toujours un verdict correct.