Planification de tâches sous contraintes

Les systèmes embarqués, en particulier les robots, ont besoin de la capacité de planifier leur prochaines actions leur offrant ainsi l'autonomie. Cependant il devient de obligatoire d'assurer un comportement sûr puisque ces systèmes interagissent de plus en plus avec des humains (par exemple : voiture autonomes, drones de loisirs, cobots manufacturiers etc.).
Afin de pouvoir résoudre ce problème en essors nous voudrions étudier la planification de tâches sous contraintes : choisir la meilleure séquence d'actions en assurant que celle-ci valide et optimise des critères variés tels que la performance et la sûreté mais il pourrait être intéressant de prendre en comte d'autres contraintes. Le but de la thèse se décompose en deux aspects majeures, le premier consiste à modéliser les contraintes s'appliquant au système dans une forme qui soit à la fois compréhensible des experts et qui puisse être exploitée par l'algorithme de planification (par exemple, en utilisant un Operational Design Domain ou un Dynamic Assurance Case pour évaluer la sûreté d'un système). Vraisemblablement cette modélisation se fera au moyen d'ontologies et de graphes de connaissances. Cela afin de bénéficier de leur grande expressivité et de l'outillage associé. Le second aspect de la thèse est l'amélioration de l'algorithme de planification afin qu'il bénéficie des modèles de contraintes, en particulier afin de bénéficier de la quantité d'information stockées dans les modèles. Ces modèles devront avoir une structure générique puisque il faut pouvoir représenter différentes natures de contraintes : sûreté, performance/coût, "confort" social, nombre de ressources contraintes sur le chemin critique, nombre et natures des interactions avec d'autres agents, faisabilité/applicabilité géométrique, (et potentiellement éthique) ...
Ce sujet s'inscrivant dans le contexte des systèmes autonomes et robotiques, une importance est donnée à l'intégration et la démonstration dans des cas réels des résultats.

Cadre formel pour la spécification et la vérification de flots de communication de processus distribués dans le Cloud

Les clouds sont constitués de serveurs interconnectés via internet, sur lesquels on peut implémenter des systèmes faisant usages d’applications et de bases de données déployées sur les serveurs. L’informatique basée sur les clouds gagne considérablement en popularité, y compris pour y déployer des systèmes critiques. De ce fait, disposer d’un cadre formel pour raisonner sur ce type de systèmes devient une nécessité. Une exigence sur un tel cadre est qu’ils permettent de raisonner sur les concepts manipulés dans un cloud, ce qui inclue naturellement la capacité à raisonner sur des systèmes distribués, composés de sous-systèmes déployés sur différentes machines et interagissant par passage de messages pour réaliser des services. Dans ce contexte, la facilité à raisonner sur les flots de communications est un élément central. L'objectif de cette thèse est de définir un cadre formel outillé dédié à la spécification et la vérification de systèmes déployés sur des clouds. Ce cadre capitalisera sur le cadre formel des "interactions". Les interactions sont des modèles dédiés à la spécification des flots de communications entre différents acteurs d'un système. Les travaux de thèse étudieront comment définir des opérateurs de structuration (enrichissement, composition) et de raffinement pour permettre de mettre en œuvre des processus de génie logiciel classique en se basant sur les interactions.

Top