Bonjour

Si vous êtes intéressés, merci de me le faire savoir de façon urgente (avant le 31/03) que je communique vos noms et prénoms à M. David Powell,
Directeur de Recherche CNRS, LAAS-CNRS, Toulouse.

Cordialement.

Catherine 

Objet : Thèse co-financée CNRS-DGA sur la validation de planificateurs

Possibilité d'une bourse financée ou co-financée par la DGA sur le sujet "Validation automatique de planificateurs pour systèmes autonomes"
Demande à faire avant le 31 mars 2008.
Peuvent faire acte de candidature les étudiants :
- de nationalité française,
- âgés de moins de 27 ans au 1er octobre 2008
- titulaires d'un Master 2 ou d'une équivalence leur permettent de s'inscrire en thèse, ou en cours de préparation à ce diplôme.

TITRE : Validation automatique de planificateurs pour systèmes autonomes


MOTS CLES : robotique ; sûreté de fonctionnement ; intelligence artificielle ; planification ; test de logiciel : satisfaction de contraintes

DESCRIPTION :

Pour des raisons de coût, de performance et de souplesse, il est fait de plus en plus appel aux systèmes autonomes et autosuffisants pour minimiser le besoin d'interventions humaines dans des applications complexes et critiques. On trouve ainsi la notion d'autonomie dans des applications telles que les satellites d'observation de la terre, les drones de surveillance et les robots de service.

La validation de systèmes autonomes utilisés dans de tels contextes est donc particulièrement cruciale. La thèse proposée est focalisée sur la
planification, une fonction centrale dans la plupart des systèmes autonomes. Aujourd'hui, la validation d'un planificateur, et plus particulièrement, son modèle de domaine caractérisant l'espace des plans possibles, repose essentiellement sur un processus de validation manuelle où l'expert du
domaine joue le rôle d'oracle de test. Une telle approche est très coûteuse dès l'instant que l'on recherche à obtenir une très bonne confiance dans la validité des plans produits. Une formalisation et une automatisation de la procédure de validation s'imposent.

Dans le cadre de cette thèse, nous proposons d’étudier d’abord des classes de propriétés permettant de juger de l'adéquation des plans produits. Ces propriétés pourraient inclure par exemple des propriétés de robustesse et de qualité des plans, ou encore des propriétés logiques non prises en compte dans le modèle de domaine. La procédure de validation pourrait ensuite se baser soit sur des preuves d’existence d’une propriété voulue (ou sa négation), soit sur une caractérisation de l’espace des solutions (par exemple, une mesure statistique du taux de succès des plans produits).
Enfin, il est clairement intéressant de proposer un retour d’expérience vers l’utilisateur lorsque la validation du planificateur échoue.