Dans le domaine de la commande de systèmes réactifs, le problème de la synthèse de contrôleur est le suivant : à partir d'une spécification du système et d'une propriété attendue de celui-ci, il s'agit de synthétiser un contrôleur qui, placé dans l'environnement et disposant de la spécification, va garantir que les exécutions possibles du système valident cette propriété. Les propriétés sont du type atteignabilité, inévitabilité, invariant, etc. Les spécifications sont en général supposées déterministes.
Malgré l'effort de vérification formelle qui peut être fait sur la spécification, les implémentations du système peuvent contenir des erreurs. Les tests qui sont constitués de séquences de contrôle et d'observation entre l'implémentation et le testeur, fournissent alors le moyen de (in)valider l'implémentation par rapport à une relation de conformité donnée. La génération automatique de tests consiste alors à générer automatiquement des tests à partir de la spécification et d'un objectif de test (qui peut être décrit par une propriété logique ou un automate). Les spécifications peuvent être non-déterministes et posséder des actions internes (non observables et non contrôlables). Dans le domaine du test de conformité de protocoles, différentes techniques permettent de produire ces tests avec des critères de longueur minimale, de contrôle optimal, etc.
On peut voir que les notions de testeur et de contrôleur sont proches. Il y a cependant quelques différences. Le problème de la synthèse n'a pas toujours de solution car le système n'est pas forcément contrôlable. La génération de test en a toujours même si le test ne pourra pas complètement contrôler le système. Il faut alors relâcher les contraintes de la synthèse (existence d'un contrôleur) pour produire un test optimal du point de vue contrôle. La vision théorie des jeux peut être utile de ce point de vue: la recherche d'un test optimal s'apparente au calcul d'une stratégie pour un jeu entre implémentation et testeur. On pourra aussi faire le lien avec la théorie du contrôle des systèmes à événements discrets de Ramadge et Wonham.
Nous proposons donc d'étudier les liens entre génération de tests et synthèse de contrôleur. Plusieurs axes de recherche en découlent :