Lieu : Irisa, Rennes
| Responsables : | Thierry JÉRON (tél. direct : 02 99 84 74 64, email : Thierry.Jeron@irisa.fr) |
|---|---|
| Hervé MARCHAND (tél. direct : 02 99 84 75 09, email : Herve.Marchand@irisa.fr) |
Mots-clés : contrôle, synthèse, test, conformité, spécification formelle, objectif de test, objectif de contrôle, système réactif.
Financement : à définir.
Sujet : Le problème de la synthèse de contrôleur consiste, à partir d'une spécification d'un système réactif et d'une propriété attendue de celui-ci, à synthétiser un contrôleur qui, placé dans l'environnement du système et disposant de la spécification, va garantir que les exécutions possibles du système valident cette propriété. La génération de tests consiste à dériver à partir d'une spécification d'un système et éventuellement d'objectifs de tests, une suite de tests. Ces tests sont ensuite exécutés sur une implémentation du système afin de déterminer sa conformité vis à vis de la spécification. Il est clair que des similitudes existent entre les deux problèmes, mais il subsiste quelques différences. Par exemple, le problème de la synthèse n'a pas toujours de solution car le système n'est pas forcément contrôlable, l'interaction est plutôt synchrone, les objectifs de contrôle sont divers (atteignabilité, inévitabilité, invariance, etc). D'un autre côté, en génération de test on cherche à maximiser le contrôle sur le système sans l'avoir complètement, l'interaction est souvent asynchrone, on se limite pour l'instant à des objectifs de tests de type atteignabilité.
L'objectif de la thèse est de contribuer à l'amélioration des techniques de synthèse de contrôleur et de génération de tests en s'appuyant sur les résultats de chacun des problèmes et en les étendant. Une piste prometteuse est de plonger ces deux problèmes dans le contexte plus général de la théorie des jeux en voyant le problème de la synthèse (respectivement de la génération de tests) comme une recherche de stratégie gagnante entre le système controlé (resp. l'implémentation) modélisé par la spécification et le contrôleur (resp. le testeur). On pourra aussi faire le lien avec la théorie du contrôle des systèmes à événements discrets de Ramadge et Wonham. Enfin, ce travail se fera en lien avec d'autres études sur la génération de tests symboliques (manipulant des données) et l'expressivité des objectifs de contrôle dans le mu-calcul.
Pour en savoir plus : http://www.irisa.fr/pampa/, http://www.irisa.fr/ep-atr/