Master 2014 2015
Stages de la spécialité SAR
Contrôle du trafic aérien : spécification et vérification de contrats 4D


Lieu :LIPN, Université Paris 13, Sorbonne Paris Cité, Villetaneuse
Encadrant : Christine CHOPPY (Paris 13), Fabrice KORDON (Paris 6), Romain KERVARC (Onera)
Dates :Mars-Avril à fin Août-début Septembre
Rémunération :gratification de stage
Mots-clés : Master SAR, autre qu’ATIAM

Description

Sujet : La notion de contrat 4D est une avancée prometteuse pour résoudre les problèmes de contrôle du trafic aérien. Un contrat 4D est une trajectoire sur un espace prédéfini à des instants donnés, et composée de deux « bulles » en mouvement : l’une (bulle de liberté) dans laquelle l’avion peut évoluer librement, et l’autre, plus grande, dans laquelle l’avion peut se déplacer en faisant attention aux autres objets (bulle de sécurité). De nombreuses propriétés importantes des contrats 4D sont à valider. L’une des plus évidentes concerne l’intersection de bulles, qui doit être vide. Un autre domaine de validation important relève des évènements ayant lieu autour d’aéroports : les contrats 4D doivent prendre en compte les pistes d’atterissage disponibles (y compris les configurations où les vents de sont pas favorables), le carburant restant dans les avions qui approchent, etc. Ceci nécessite la coopération de l’aéroport et il peut y avoir des conflits à traiter. Les contrats 4D doivent être planifiés à l’avance pour un espace aérien donné. Cependant, ils doivent être adaptés en temps réel à la situation lorsqu’ils sont exécutés. Des réajustements de contrats 4D peuvent comprendre :
- l’évitement d’une zone de météo trop dangereuse,
- l’augmentation de la taille d’une bulle lorsque la météo est moins favorable mais pas trop dangereuse,
- des modifications locales (à court ou long terme sur la trajectoire) pour éviter de se rapprocher d’un autre avion (qui peut lui-même être amené à également modifier son contrat 4D),
- le changement de la direction d’approche d’un aéroport (suite à la météo, la saturation de pistes, etc.),
- dans de plus rares cas (qui ne doivent avoir lieu que lorsqu’un problème majeur est survenu), le changement de l’aéroport de destination, le changement drastique d’horaires, etc.
- lorsque l’embarquement est retardé ou lorsque l’aéroport de départ est saturé, le départ retardé pour réajuster, par rapport aux autres avions, les horaires de décollage et les routes,
- la prise en compte de changements spécifiques dûs à des avions proches en détresse (libérer une route, etc.). Dans ce stage, il s’agit d’analyser ce problème et d’en modéliser formellement une partie afin de pouvoir ensuite appliquer des méthodes de model checking sur le modèle formel résultant. La modélisation sera effectuée dans un formalisme tel que celui des réseaux de Petri colorés, et sera centrée sur certains des conflits décrits ci-dessus. Ce stage s’intègre dans une collaboration entre l’ONERA, l’Université Paris VI (Prof. Fabrice Kordon), et l’Université Paris 13 (Prof. Christine Choppy). Les candidats devront avoir des connaissances dans les domaines des méthodes formelles et de la modélisation, et devront être dans leur dernière année de Master (ou équivalent).