Une machine pour penser l'homme
Prendre en compte les comportements humains pour le bon fonctionnement des systèmes
Contexte
En informatique, il existe différentes méthodes pour s'assurer du bon fonctionnement de systèmes, notamment la preuve mathématique et le test. Ces méthodes sont utilisées pour des systèmes dits critiques dans les transports et le nucléaire, par exemple. Elles permettent de garantir que le système technique répondra correctement aux commandes qui lui sont données. Mais ces méthodes ne peuvent pas prendre en compte d'éventuelles mauvaises utilisations par les opérateurs humains. Or de nombreux cas d'étude montrent que certains dysfonctionnements sont dus à des erreurs humaines, souvent liées à une mauvaise compréhension par l'humain de ce que fait le système.
Objectif
L'objectif de ce projet de recherche est de proposer un nouveau modèle informatique pour étudier la fiabilité des systèmes critiques en prenant en compte la part d'erreur humaine dans l'utilisation du système. Il s'agit de "modéliser" les perceptions et le raisonnement d'un être humain qui interagit avec un système, c'est-à-dire d'en faire un modèle mathématique qui peut être testé de manière automatique, soit par des outils de preuve mathématique, soit par des outils de test. Ainsi, nous voulons prévoir les éventuels dysfonctionnements dus aux erreurs humaines. Il sera ainsi possible de corriger le système ou son interface homme-machine, ou d'adapter la formation des opérateurs pour éviter ces erreurs.
Méthode
La méthode envisagée pour traiter ce problème est d'utiliser des modèles mathématiques et logiques (règles de raisonnement pour l'humain, modèles du comportement du système, règles d'interaction entre l'humain et la machine) afin de pouvoir explorer automatiquement les comportements possibles de l'humain et de la machine en interaction. Ces méthodes sont développés en Intelligence Artificielle et en Génie Logiciel. Il s'agit de modèles mathématiques qu'on appelle "logiques modales".
Concrètement, il s'agira dans un premier temps de concevoir un cadre formel qui combine deux logiques modales: la logique BDI (utilisée pour représenter et raisonner sur les croyances et les intentions des humains), et la logique temporelle LTL (utilisée pour la vérification formelle de systèmes critiques). Une technique de vérification pour ce cadre formel sera ensuite développée et implémentée dans un outil informatique.
Une partie expérimentale traitant plusieurs cas d'études (accidents d'avion par exemple) permettra de valider les modèles théoriques. Elle donnera lieu à la réalisation de programmes mettant en œuvre les modèles pour reconstruire les scénarios connus de ces cas d'étude.
Ce que vous apprendrez dans ce projet
- Concevoir et utiliser des modèles mathématiques et logiques.
- Mettre en œuvre des outils informatiques pour prouver des propriétés d'un modèle.
- Utiliser l'ingénierie dirigée par les modèles pour outiller votre démarche.
- Valider expérimentalement vos modèles théoriques.
- Prendre part à la vie d’une équipe de recherche.
- Contribuer à des avancées à la frontière entre Intelligence Artificielle et Ingénierie Logicielle.
Contact
Cette étude est portée par le LRI et le LIMSI, deux laboratoires d'informatique de l'université Paris-Saclay.
- Frédéric Boulanger frederic.boulanger@lri.fr
- Nicolas Sabouret nicolas.sabouret@limsi.fr
- Safouan Taha safouan.taha@lri.fr
Les trois chercheurs sont aussi enseignants au département informatique de CentraleSupélec, campus de Gif.