Soutenance mémoire
Les composants matériels
Nous présentons ici les composants matériels du drone, avec un focus sur les capteurs de position. Certains drones sont aussi équipés de matériels qui ne sont pas présentés ici, comme le capteur de courant électrique, l’équipement de stabilisation de carte, etc. Ces composants apportent plus de possibilités au drone mais entraînent aussi plus de consommation d’énergie et plus de poids pour le drone. Les bons matériels conditionnent souvent un vol plus long et permettent de porter des objets plus lourds. Le moteur. Le moteur transforme une énergie électrique en énergie mécanique. Les drones Quadrotor disposent de quatre moteurs ; les Hexarotors disposent de six moteurs. En fonction du moteur, le drone est plus puissant, il peut voler plus haut et plus rapidement ; et dans certains types de perturbations il est plus stable. Les drones Hexarotors peuvent voler avec quatre moteurs lors de défaillances matérielles ; Ils sont plus puissants et peuvent porter les objets lourds en volant. La batterie. La batterie est la source d’énergie du drone. Les drones sont toujours équipés d’au moins une batterie. Dans les situations non désirées, par exemple quand le drone tombe, c’est souvent la batterie qui endommage le drone et le rend irrécupérable. La télécommande. La télécommande est destinée au pilote, mais les drones automatiques peuvent aussi être équipés d’une ou plusieurs télécommandes afin qu’un humain puisse prendre la main dans les situations d’urgence. Les LED. Les lumières sur un drone sont à base de LED. Tous les drones ne sont pas équipés en LED mais c’est un composant pratique pour trouver la position du drone visuellement dans la nuit. La carte barométrique. La carte barométrique est aussi appelée altimètre. Elle agit comme un capteur pour le drone. Son rôle est de mesurer l’altitude à l’aide de la pression atmosphérique. Ce composant est particulièrement critique car il génère beaucoup de bruit, qui peut perturber les mesures de position. Le compas. Le compas est un capteur du drone qui donne une référence de direction (le nord) sur le plan horizontal et permet ainsi la mesure d’angles horizontaux par rapport à cette direction. Le GPS. Le GPS (Global Positioning System) est un capteur du drone qui consomme plus d’énergie que les autres. Il utilise un système de positionnement par satellites appartenant au gouvernement des États-Unis. Les signaux transmis par les satellites peuvent être librement reçus et exploités par quiconque. Il est un peu plus lent que les autres capteurs, mais il est plus stable et a un bon fonctionnement sur une grande trajectoire extérieure. L’accéléromètre. L’accéléromètre est un capteur qui permet de mesurer l’accélération linéaire du drone. Il s’agit en fait de 3 accéléromètres qui calculent les accélérations linéaires selon 3 axes orthogonaux. L’accéléromètre est sensible aux perturbations, mais il est rapide, précis, et en l’absence de perturbations, ses performances sont constantes dans le temps. Le gyroscope. Le gyroscope est un capteur qui mesure la position angulaire et l’orientation par rapport à un inférentiel inertiel. Il consomme moins d’énergie que les autres capteurs, il est rapide et précis, mais il souffre des erreurs d’intégration, c’està-dire qu’il a un bruit qui augmente avec le temps. Il est complémentaire à l’accéléromètre.
Un aperçu du modèle de drone final
Le modèle global du système de contrôle de vol du drone est présenté dans la Figure 5.1. Le but de ce modèle est de représenter les calculs qui ont lieu dans le contrôleur de vol (FCS – Flight control system) afin d’adapter la trajectoire du drone au plan de vol prévu, aussi bien en fonction des imprécisions des estimations des mesures de position et d’orientation, que des perturbations par le vent. Nous utilisons le modèle pour calculer les positions du drone et compter le nombre de simulations qui entrent dans une zone de sécurité donnée, en fonction des paramètres. Dans ce modèle, la position exacte du drone est encodée avec ses deux coordonnées dans le plan. En effet, le plan de vol est établi sans prendre en compte l’altitude dans la plupart des cas. Ces coordonnées sont ensuite comparées avec celles décrivant le plan de vol pour décider à quelle zone de sécurité elles correspondent. Dès que le drone a atteint une zone interdite (les zones 4 ou 5), le calcul s’arrête, sinon il continue jusqu’à épuiser le temps de parcours correspondant au plan de vol. Le modèle utilise plusieurs paramètres probabilistes : les paramètres FilterProba1, FilterProba2, FilterProba3, FilterProba4 et FilterProba5 (figure 5.1) représentent la précision de la position et de l’orientation estimées par le filtre et les capteurs. Le choix probabiliste résultant, représenté dans la boîte étiquetée Filter Computation (figure 5.1) donne alors la distance entre la position exacte du drone et celle estimée par les capteurs et le filtre. Ce choix est suivi par un calcul dans la boîte étiquetée Safety Zone Computation (voir Figure 5.1) qui détermine les coordonnées exactes de la prochaine position du drone, et permet de décider à quelle zone de sécurité appartient cette position. Lorsque le vent n’est pas pris en compte, le résultat de ce calcul est suffisant pour décider si le modèle doit poursuivre son déroulement. Lorsque le vent est pris en compte, une autre étape suit. Elle est indiquée par la boîte étiquetée Wind Computation; d’autres paramètres probabilistes y sont utilisés pour décider de la force du vent (nous supposons une direction constante) et une nouvelle position tenant compte de ces perturbations est calculée. Finalement, la zone de sécurité à laquelle appartient cette dernière position est calculée. Pour une durée de temps (T) donnée, nous effectuons, en fonction de la fréquence du filtre considéré, plusieurs itérations du calcul de la position du drone et la simulation s’arrête dès qu’il arrive dans un état des zones de sécurité interdites. Notons que la fréquence du filtre (f) ainsi que les positions et distances des points de contrôle dans le plan de vol sont données comme entrées du modèle. La position du point de contrôle dans le plan de vol permet de calculer la vitesse du drone, alors que la fréquence du filtre permet de fixer le nombre d’estimations de positions qu’il y aura dans un plan de vol donné (i.e. le nombre maximum d’itérations que le modèle doit effectuer). Ce modèle permet ainsi de simuler l’évolution des drones pour un plan de vol et pour des paramètres choisis. Les résultats des simulations sont exploités pour analyser le comportement du drone et régler ainsi les valeurs des paramètres, afin d’obtenir le minimum d’entrées dans les zones de sécurité interdites.
Mise en œuvre de la version 2 avec le model checker PRISM
Nous avons implémenté notre modèle pour les versions 1, 2 et 3 avec l’outil PRISM. La première version est simple, elle engendre un automate qui ne comporte que 31 états et 55 transitions. La taille de la deuxième version dépend de Tchemin (le temps total du trajet en s) et Treponse (le temps de réponse en s). Nous fixons Treponse = 1, l’outil doit donc simuler Tchemin fois le filtre pour un trajet donné. Les nombres d’états et de transitions pour différentes instances de la version 2 sont présentés dans la Table 6.1. Notons que ces nombres sont multipliés par 4 lorsque Tchemin = 2. En réalité, notre IMU envoie la position toutes les 0,025s (ce qui correspond à une fréquence de f = 40Hz). Pour un trajet de 10s, il faut donc 400 boucles d’estimation de la position du drone, ce qui correspond à Tchemin = 400 si nous conservons Treponse = 1. Pour un trajet d’une minute, 2400 boucles sont alors nécessaires. La version 3 du modèle prend aussi en compte la dernière position corrigée du drone. La taille des zones et la position du drone ne sont donc plus des constantes dans le modèle mais des variables. PRISM n’est alors plus capable de faire la simulation car ces variables ne sont pas bornées. Par exemple, supposons que zone1 ∈ [0, 20], zone2 ∈ (20, 40], zone3 ∈ (40, 60], zone4 ∈ (60, 80], zone5 ∈ (80, +∞]. Nous ne pouvons pas définir les variables avec PRISM car zone5 n’est pas bornée. Nous choisissons donc zone5 ∈ (80, 100]. L’unité pour la taille des zones est le décimètre, car le mètre nécessite des nombres décimaux, ce qui ralentit le calcul. En centimètres les valeurs sont encore plus grandes, ce qui augmente le nombre d’états. Nous supposons un trajet de 50m (500dm) en 5min avec (Treponse = 1, Tchemin = 300s). Même en ne prenant pas en compte le temps de réponse de l’IMU Treponse = 0.025s, le nombre d’états et de transitions est trop grand. Ainsi, pour l’expérimentation avec un trajet de 50m, nous n’avons pas des nombres d’états et de transitions exacts à donner car nous n’avons pas pu finir ce test avec PRISM. En effet, après deux heures d’attente pour un test avec Tchemin = 5s et Treponse = 1s, nous avons décidé de changer d’outil et donc de méthode
Comparaison des versions 4, 6 et 7 en MCpMC
Les versions 4 à 7 du modèle sont présentées dans la section 5.9. Pour rappel, la version 4 améliore la version 3 en prenant en compte les erreurs d’estimation sur l’axe x en plus de celles sur l’axe y. Dans la version 5, nous avons de plus intégré les potentiels changements d’objectifs lorsque le drone est en retard sur sa trajectoire. Finalement, les versions 6 et 7 intègrent les perturbations liées au vent en tant que constantes dans la version 6 puis en tant que paramètres dans la version 7. Comme vu précédemment, les polynômes obtenus en sortie sont trop longs pour être comparés ou analysés manuellement. Nous ne présentons donc pas les polynômes obtenus lors d’expérimentations réalistes, mais plutôt leur évaluation pour différentes valeurs des paramètres ProbaFilter1-ProbaFilter5 (PF1-PF5). Une comparaison centre les versions 6 et 7 a été faite avant de développer la version 8 du modèle. Le but était de savoir si la version 8 de notre modèle devait se baser sur la version 7 ou la version 6. Les versions 6 et 7 sont deux versions développées en parallèle. La version 6 est plus rapide, mais dans la version 7 le vent est en paramètre dans le polynôme. Nous définissons deux scénarios afin d’évaluer nos polynômes. Le scénario 1 est un scénario proche de la réalité. Le scénario 2 est pour voir plus clairement l’impact des paramètres. Pour le scénario 1 PF1 = 0.15, PF2 = 0.3, PF3 = 0.4, PF4 = 0.1 et PF5 = 0.05. Pour le scénario 2 PF1 = 0.1, PF2 = 0.25, PF3 = 0.35, PF4 = 0.2 et PF5 = 0.1 . Dans ces deux scénarios, la zone de sécurité 4 est située à 8m et la zone de sécurité 5 est située à 50m de la zone de vol. PF1-PF5 correspond à la probabilité que l’écart entre la position effective et la position estimée soit de [0, 2] mètre pour PF1, de (2, 4] mètres pour PF2, de (4, 6] mètres pour PF3, de (6, 8] mètres pour PF4 et de (8, 10] mètres pour PF5. D’après l’expert de PIXIEL, le bruit des capteurs peut aller jusqu’à 10 mètres, mais grâce au filtre, la vitesse et la distance de correction réduisent l’erreur. Les bruits dépendent aussi de l’environnement de vol et de la qualité des composants du drone. Les éléments de l’environnement peuvent aussi perturber les drones. Par exemple lors d’un spectacle de drones, si des spectateurs oublient d’éteindre le WIFI ou le point d’accès de leur smartphone, les signaux interférent avec les drones. Le scénario 1 est plus réaliste que le scénario 2. Pour des drones ayant des composants de qualité, la probabilité PF1 devrait être plus grande et PF3 plus petite, mais à cause de mauvais résultats des expérimentations sur la chaîne de production utilisée, nous ne pouvons pas fournir de valeurs exactes. Dans les simulations des versions 6 et 7, les paramètres liés au vent correspondent à la probabilité d’avoir une force de vent de [0, 20] km/h, (20, 30] km/h, (30, 50] km/h et (50, 70] km/h respectivement ; nous les avons définis à 0.55, 0.43, 0.01 et 0.01 (ce qui correspond aux conditions typiques de la ville de Nantes). La direction du vent est toujours face au drone (direction identique dans tous les repères utilisés). Dans la Table 6.4, nous avons synthétisé les résultats pour 10k, 20k et 50k simulations des versions 4, 6 et 7 de notre modèle en fixant Tchemin = 5s et Treponse = 1s. V1 et V2 représentent deux expériences avec les mêmes données afin de comparer les résultats obtenus. Dans chaque case, nous avons calculé la probabilité et l’intervalle de confiance pour les valeurs des paramètres de chacun des scénarios identifiés cidessus. Avec les valeurs des paramètres que nous avons choisies pour l’évaluation de nos polynômes, nous observons que les probabilités obtenues pour le scénario 1 sont plus faibles que celles obtenues pour le scénario 2. L’intervalle de confiance pour le scénario 1 est aussi plus faible. Cet intervalle est aussi un polynôme qui change avec les valeurs que nous avons données. Nous observons aussi que les versions 4 et 6 ont un temps d’exécution beaucoup plus rapide comparé à la version 7 dans laquelle la force du vent est paramétrique. L’augmentation du nombre de paramètres ralenti en effet le temps de calcul de la version 7 qui doit de plus faire plus de simulations pour obtenir un niveau de précision similaire. Pour cette raison, nous avons choisi de baser notre version 8 sur la version 6 (dans laquelle le vent est pris en compte de manière non paramétrique).
|
Table des matières
Introduction
1 Contexte de la thèse
2 Les composants, le fonctionnement et les problématiques d’un drone
2.1 L’attitude du drone
2.2 Les composants d’un drone
2.2.1 Les composants matériels
2.2.2 Les composants logiciels
2.3 La règlementation en matière de drones
2.4 Problématiques du drone
2.4.1 Les défaillances matérielles et logicielles
2.4.2 Les zones de sécurité
3 Problématique de la de thèse et état de l’art sur la modélisation et la vérification des systèmes de drones
3.1 Problématiques et orientations de la thèse
3.2 État de l’art sur la modélisation et la vérification des systèmes de drones
4 Modélisation formelle et vérification
4.1 Chaînes de Markov
4.2 Chaînes de Markov paramétrées (pMC)
4.3 Model Checking Statistique
4.4 Model Checking Statistique Paramétrique (pSMC)
4.5 Les outils de model checking
4.5.1 PRISM
4.5.2 PARAM
4.5.3 MCpMC
5 Méthode de modélisation formelle de drones civils
5.1 Un aperçu du modèle de drone final
5.2 Méthode de construction du modèle
5.3 Modèle du drone à l’aide d’une chaîne de Markov
5.4 Première version du modèle (en PRISM)
5.5 Calcul de la position par rapport aux zones de sécurité
5.6 Deuxième version : prise en compte des zones de sécurité
5.7 Expérimentations sur une chaîne de production
5.8 Troisième version : prise en compte de la distance exacte
5.8.1 Le modèle construit pour PRISM
5.8.2 Le modèle construit en Python pour utiliser la méthode pSMC
5.9 Versions 4 à 7 avec la méthode pSMC
5.10 Version 8 avec la méthode pSMC : prise en compte de longs trajets
6 Expérimentations et interprétations
6.1 Implémentation
6.1.1 Mise en œuvre de la version 2 avec le model checker PRISM
6.1.2 Mise en œuvre de la version 3 avec l’outil MCpMC
6.1.3 Comparaison des versions 4, 6 et 7 en MCpMC
6.1.4 Mise en œuvre de la version finale (version 8) avec MCpMC
6.2 Réduire la probabilité d’entrer en zone interdite
6.2.1 Réduction du nombre de points sur une ligne droite
6.2.2 Allongement du temps des trajets
7 Conclusion
Bibliographie
8 Annexe
Télécharger le rapport complet
