Le problème abordé dans cette thèse concerne le test de cartes mixtes en maintenance. Dans le domaine du test matériel, de nombreuses méthodes et outils de test existent, ciblant principalement le test de circuits en phase de conception et de production. Peu d'intérêt a été porté jusqu'à présent au test de cartes mixtes en phase de maintenance. Pourtant, certains systèmes comme par exemple les systèmes militaires doivent rester opérationnels pendant plusieurs décennies. Il est alors important de s'assurer que les fonctionnalités des cartes électroniques composant ces systèmes ne se dégradent pas au cours du temps. D'autre part, lorsqu'une carte est en panne, une aide au diagnostic s'avère précieuse lorsqu'il faut réparer. Nous proposons une méthodologie de test fonctionnel adaptée au contexte de la maintenance. Cette méthodologie permet une modélisation fonctionnelle uniforme des composants analogiques, numériques et mixtes de la carte à tester et est flexible vis-à-vis de la quantité d'informations disponibles sur la carte. La génération des données de test est pilotée par des stratégies de test globales (bien adaptées à la maintenance préventive) ou locales (plus appropriées dans le cas de la maintenance corrective). L'expertise et les pratiques industrielles des ingénieurs de test en maintenance, qui sont indispensables, sont prises en compte par la méthodologie sous la forme de modèles de test et de tactiques de test qui précisent le processus de génération des données de test. La méthodologie proposée est implantée dans un outil prototype en utilisant la programmation logique par contraintes, et son application sur quelques exemples de cartes mixtes est discutée.

Le problème abordé dans cette thèse concerne la productionautomatique de données de test permettant de prouver des propriétés de programmes. Nous nous situons ainsi à mi-chemin entre le domaine du test et celui de la vérification de programmes. Les travaux dans le domaine du test ont conduit à des outils semi-automatiques d'utilisation simple, mais qui reposent sur des hypothèses difficilement vérifiables en pratique. Dans le domaine de la vérification, des outils basés sur des méthodes formelles ont été développés, mais ils nécessitent un utilisateur expert dans les techniques de preuve utilisées par l'outil. Cette situation est due aux problèmes d'indécidabilité engendrés par la puissance des formalismes traités. La thèse que nous présentons est qu'il est possible de développer des méthodes formelles automatiques pour prouver des propriétés de programmes, à condition de considérer des formalismes restreints. Notre principale contribution est une nouvelle approche pour la vérification de programmes, intégrant les techniques de test et d'analyse statique. Nous proposons une méthode formelle de génération de jeux de test finis complets permettant de prouver qu'un programme vérifie une propriété donnée. Cette méthode utilise le texte du programme et de la propriété, qui doivent appartenir à certaines classes de programmes (ou de propriétés). Ces classes sont représentées par des hiérarchies de schémas, qui peuvent être vues comme modélisant des hypothèses de test. Tout programme appartenant à un de nos schémas et passant le jeu de test avec succès vérifie la propriété testée. Pour une propriété donnée, notre méthode est complètement automatique et ne nécessite donc aucune compétence particulière de l'utilisateur. Nous avons implanté cette méthode dans un prototype (traitant un langage fonctionnel restreint), pour le cas de propriétés s'exprimant en termes de longueurs de listes.