Soutenance de thèse de Rim Saddem, le 20 juin 2019, à 10:30, au LIRMM

Publié le par

Model-checking pour l’agriculture de précision

Thèse soutenue le jeudi 20 juin 2019 à 10:30
Lieu : Laboratoire d’informatique, de robotique et de microélectronique de Montpellier, 161 Rue Ada, 34095 Montpellier
Salle : « Jean-Pierre Nougier »

Rim Saddem

Composition du jury proposé

  • M. Didier CRESTANI, IUT Montpellier-Sète/UM, Directeur de thèse
  • M. Frédéric GARCIA, INRA TOULOUSE, Rapporteur
  • M. Laurent PIERTRAC, INSA de Lyon, Rapporteur
  • M. Roland LENAIN, IRSTEA Clermont-Ferrand, Examinateur
  • M. Olivier NAUD, IRSTEA Montpellier, Co-encadrant de thèse
  • Mme Karen GODARY-DEJEAN, Polytech Montpellier/UM, Co-encadrant de thèse

Résumé :
L’agriculture de précision (AP) s’est fortement développée au cours des dernières décennies avec les progrès des technologies de localisation, des capteurs et des techniques de télédétection. Le principe de l’AP est de rechercher et mettre en œuvre la Bonne action au Bon moment et au Bon endroit (« 3B »), avec l’objectif d’améliorer l’efficience de l’agriculture suivant les critères d’une agriculture durable. Nous considérons dans cette thèse l’évaluation de la faisabilité d’opérations agricoles vis à vis de critères relevant de l’AP, en faisant appel à des techniques de modélisation et de vérification formelles. Pour modéliser et vérifier ces opérations, une représentation des dynamiques temporelles et spatiales est nécessaire. Le model-checking de systèmes d’automates temporisés avec des requêtes dans une logique temporelle arborescente répond à ces besoins, les positions spatiales pouvant être représentées de façon ad-hoc dans le cadre de ces formalismes. Trois exemples d’opérations agricoles sont considérés dans ce mémoire. La première est relative au calcul d’une séquence optimale de commandes pour une pulvérisation de précision en viticulture. La seconde concerne la récolte sélective en viticulture. La dernière est relative à la vérification d’une mission de robotique agricole. Nous étudions dans ces exemples l’atteignabilité d’un état cible pour l’opération, ou l’atteignabilité avec un critère de coût optimal. Pour pallier au problème d’explosion combinatoire rencontré dans les cas traités, une méthodologie de décomposition pour le model-checking d’atteignabilité a été développée. Les résultats expérimentaux avec et sans décomposition sont présentés pour les 3 exemples d’opération étudiés. La technique de décomposition est appliquée sur 2 des 3 exemples et les résultats expérimentaux montrent son efficacité.

Motsclés: systèmes à événements discrets,synthèse de contrôleur,décomposition,agriculture de précision, model checking, optimisation

Share