Contact: frederic.boulanger@centralesupelec.fr
Frédéric Boulanger, CentraleSupélec/LRI
Formalisation d'algorithmes
Durée : de 2 à 3 semestres
Nombre d'élèves : jusqu'à 4
Contexte
Le bon fonctionnement de nombreux systèmes dépend de la correction des algorithmes qu’ils utilisent, et du fait que ces algorithmes terminent et ne s’exécutent pas indéfiniment. Il existe des théories qui fournissent un cadre mathématique pour prouver la correction et la terminaison d’algorithmes et de programmes, mais la certitude la plus absolue n’est obtenue qu’en éliminant toute étape « intuitive » dans les raisonnements. Il existe des programmes qui vérifient mécaniquement la correction d’une preuve, et de nombreux algorithmes ont ainsi pu être prouvés formellement.
Ce projet est une initiation à la vérification formelle d’algorithmes, avec pour objectif d’identifier les méthodes et les types de modèles qui fonctionnent le mieux pour différentes structures de données et différents types d’algorithmes.
Objectifs du projet
Ce projet a deux objectifs : permettre aux élèves de se familiariser avec les systèmes de preuve formelle, et dégager des motifs récurrents dans la structure des bonnes preuves afin de proposer une méthodologie pour la modélisation des structures de données et la vérification de programmes. La principale difficulté est d’identifier les bons patrons de conception qui permettront d’aborder plus facilement la vérification d’algorithmes et d’automatiser partiellement la construction des modèles des structures de données.
Étapes du projet
Dans une première partie, on se familiarisera avec les outils de preuve tels que Why3 [http://why3.lri.fr] et Isabelle/HOL [https://isabelle.in.tum.de]. Ce sera l’occasion d’étudier comment sont modélisées les structures de données et les algorithmes pour lesquels des preuves formelles existent déjà.
Dans un deuxième temps, on cherchera à identifier ce qui est factorisable dans les différentes preuves étudiées : modélisation des structures de données, types de lemmes utilisés, structure des dépendances entre les différents théorèmes. On vérifiera alors que ces éléments sont transposables à des preuves d’autres algorithmes sur les mêmes structures de données, ou à des structures de données différentes. Ceci devrait mener à la définition d’une méthodologie permettant de guider la définition des structures de données, les types de lemmes à démontrer sur ces structures, et leur utilisation pour la vérification des algorithmes.
Enfin, selon la durée du projet et les résultats obtenus lors des étapes précédentes, on pourra appliquer ces résultats à un outil permettant de vérifier des programmes C en tenant compte de l’architecture matérielle sur laquelle le code est utilisé. Ceci introduit une complexité supplémentaire, mais est indispensable vu la nature des bugs trouvés récemment sur certaines architectures matérielles.
Compétences acquises
Connaître différentes structures de données et algorithmes, les techniques de preuve formelle
Maîtriser divers outils de preuves
Savoir modéliser un problème en logique d’ordre supérieur
Être capable d’identifier des patrons de conception de modèles logiques et d’automatiser partiellement leur mise en œuvre
Domaine concerné
Vérification de programmes
Bibliographie
- http://people.irisa.fr/David.Pichardie/agreg/doc/preuvealgo.pdf
- http://www-verimag.imag.fr/~wack/ALGO5/Cours03.pdf
- http://numerisation.univ-irem.fr/WR/IWR10007/IWR10007.pdf
Modélisation de comportements humains
Durée : de 2 à 3 semestres
Nombre d'élèves : jusqu'à 4
Contexte
S'il existe des méthodes pour prouver la correction d'un programme, il reste difficile de prouver qu'un être humain l'utilisera correctement. Ce projet vise à modéliser le comportement d'humains qui interagissent avec des systèmes.
On s'appuiera sur une logique modale de type BDI (Beliefs, Desires, Intentions) qui cherche à décrire le comportement d'un humain en supposant qu'il a des croyances, qui peuvent être mises à jour en fonction de son expérience, des désirs qu'il cherche à satisfaire, et des intentions, qui sont un ensemble cohérent d'objectifs à atteindre pour satisfaire les désirs.
Objectifs du projet
L’objectif du projet est d’une part de se familiariser avec les techniques de modélisation de comportements humains (logiques modales, modèles multi-agents), et d’autre part de définir une méthode permettant de prédire les comportements humains qui conduisent à un échec (crash d'avion, erreur médicale etc.) alors que les systèmes utilisés fonctionnent correctement. Ces prévisions pourraient permettre soit d'améliorer l'ergonomie des systèmes, soit d'améliorer la formation des opérateurs.
La difficulté de ce deuxième objectif est due à la complexité des comportements humains et à la nécessité de trouver les bonnes abstractions pour être capable de les étudier sans les rendre triviaux.
Étapes du projet
La première étape du projet sera de se familiariser avec la logique BDI, notamment en écrivant en Python ou en Java un simulateur permettant de reproduire des comportements simples.
Selon le goût des élèves pour la logique et la preuve, on pourra implanter formellement ce modèle dans un assistant de preuve tel qu’Isabelle/HOL [https://isabelle.in.tum.de] afin d'en prouver des propriétés.
La suite du projet sera consacrée à l’amélioration du modèle pour prendre en compte les aspects temporels (certaines actions ne sont pas instantanées), la mise à jour des connaissances au fil des interactions de l’humain avec son environnement, la modélisation des certains traits de caractère (être têtu, audacieux, prudent etc.) afin d’identifier un maximum de cas d’interactions homme-machine.
Compétences acquises
Connaître différentes techniques de modélisation des comportements humains
Maîtriser les logiques modales pour prendre en compte l’influence du contexte sur la véracité d’une proposition
Savoir modéliser des comportements complexes à partir de règles simples
Être capable de construire un modèle de comportement et l’implémenter dans un simulateur
Domaine concerné
Modélisation des comportements humains