|
Synthèse de contrôleurs et génération de tests
Localisation :Irisa, Rennes
Reponsables : 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/
File translated from TEX
by TTH,
version 2.25.
On 8 Mar 2000, 15:33. |