Contexte
Cette étude se situe dans le contexte des travaux de recherche qui sont menés d'une part au sein du LRI en modélisation et vérification de systèmes, et d'autre part au LIMSI en modélisation et simulation du comportement humain par des chercheurs de ces laboratoires qui sont également enseignants au département informatique de CentraleSupélec.
Les travaux de ces deux équipes ont en commun d'utiliser des logiques modales, qui constituent un bon compromis entre la logique propositionnelle (qui est peu expressive mais facile à vérifier) et la logique du premier ordre (qui est très expressive mais indécidable). Cependant, les modèles diffèrent par leur utilisation : pour la vérification de système, on s'intéresse aux aspects temporels pour décrire des propriétés portant sur le comportement dynamique du système ; en intelligence artificielle, les logiques modales sont utilisées pour décrire des intentions et/ou des émotions d'agents intelligents simulant des humains. Notre objectif est de combiner les approches en IA avec les méthodes formelles pour modéliser et vérifier des systèmes complexes intégrant des composants techniques (logiciels) et des utilisateurs humains. En d'autres termes, il s'agit d'intégrer le facteur humain dans la modélisation et la vérification de systèmes.
Objectif
Dans le cadre de cette étude, nous travaillerons sur un scénario bien défini inspiré d'incidents survenus en aviation civile dans le cadre de la gestion du trafic aérien. L'objectif de l'étude est de :
- Proposer une représentation logique du système, décrivant les états possibles (croyances des pilotes ou de la tour sur des intervalles temporels) et les transitions du système (messages entre la tour de contrôle et les avions, événements ou actions des pilotes) ;
- Décrire des situations d'erreur ;
- Implémenter un simulateur très simple capable, à partir d'un état initial, de dérouler un scénario d'exécution ;
- Implémenter une interface graphique permettant de visualiser et de contrôler cette exécution.
L'analyse du modèle logique du système pourra se faire soit à l'aide de solveurs existants, soit en développant un solveur ad hoc, soit en utilisant conjointement différents outils logiques.