Loading...
 
[Show/Hide Left Column]

ASTHME : 

Analyse statique de systèmes hybrides 

décrits par des modèles exécutables


Début : 2012
Axe : ScilEx
Sujet : Définition de méthodes de vérification formelle pour les modèles de programmes de contrôle-commande.
Directeurs : Alexandre CHAPOUTOT, ENSTA / Olivier BOUISSOU, LIX / Michel KIEFFER, L2S
Institutions : ENSTA ParisTech, CEA (LIST), Université Paris Sud
Laboratoire gestionnaire : ENSTA
Doctorant : Adel DJABALLAH
Lien vers HAL : Thèse Adel Djaballah - 03/07/2017

Productions scientifiques:

Contexte:
Pour des besoins de sécurité, de protection de l'environnement ou pour le confort, l'automatisation des fonctionnalités est la solution adoptée de plus en plus dans l'industrie, en particulier les domaines des transports et de l’énergie. L'automatisation se traduit par l'utilisation de composants électroniques pilotés par des programmes informatiques qui deviennent de plus en plus complexes. En effet, les fonctions qu'ils remplissent sont de plus en plus nombreuses et de plus en plus interconnectées, par exemple un contrôleur de vitesse couplé avec un détecteur anti-collision.

La contrepartie de cette automatisation est l'utilisation de programmes informatiques pour des tâches critiques, c'est-à-dire dont la conséquence d'une défaillance peut être catastrophique. Par exemple, le régulateur de vitesse d'une automobile a un comportement assez simple, intuitivement le conducteur fixe une vitesse à maintenir et le programme informatique en fonction de la vitesse du véhicule et de cette vitesse à maintenir pilote les commandes d'accélération et de freinage de la voiture pour remplir l'objectif désiré. Cependant, une défaillance de ce programme informatique peut entraîner un accident dont la conséquence pourrait être le décès d'automobilistes. La conception de tels programmes informatiques est donc très contrainte afin de garantir leur bon fonctionnement. A noter de plus, que ces contraintes de sûreté s'ajoutent aux contraintes économiques qui demandent d'aller toujours plus vite pour répondre aux besoins du marché.

Les programmes informatiques évoqués précédemment font partie de la famille des programmes de contrôle-commande, ce qui signifie qu'ils permettent d'amener un système vers un état désiré. La particularité de ces programmes est d'interagir continûment avec un environnement physique, par exemple la vitesse d'une automobile dans le cas du régulateur de vitesses. Cette interaction met en relation deux mondes qui évoluent différemment dans le temps. Le premier est celui de l'environnement physique qui évolue continûment dans le temps. Le second est celui des programmes informatiques qui évoluent de manière cadencée dans le temps. Le terme système hybride est alors utilisé pour décrire l'étude de programmes avec la prise en compte de leur environnement physique.
Pour continuer avec l'exemple du régulateur de vitesse, l'exécution d'un tel programme est défini par les étapes suivantes: accéder à la vitesse courante de la voiture (grâce à des capteurs), prendre la décision d'accélérer ou de freiner, effectuer l'action associée à la décision (grâce à des actionneurs). Ces trois étapes sont répétées à fréquence constante, toutes les 10ms par exemple. La conséquence de la prise de décision par le programme d'accélérer ou de freiner entraîne une modification de la vitesse courante de la voiture qui va par la suite influencer les prises de décisions ultérieures. Le défi dans la mise en oeuvre de tels programmes est donc de comprendre l'interaction fine qu'il existe entre un programme et son environnement d'exécution. Image

Objectif scientifique:
Les méthodes de vérification formelle permettent d'accroître la confiance dans le fonctionnement logiciel en apportant une preuve mathématique de son comportement. Elles conduisent à l'élaboration d'outils automatiques, c'est-à-dire de programmes informatiques qui vérifient d'autres programmes informatiques. L'automatisation de la vérification permet de gérer la complexité croissante des programmes et ainsi de répondre également aux contraintes économiques.

Une difficulté de mise en oeuvre des outils de vérification formelle est de pouvoir être adopté par les industriels dans leurs processus de développement. Plus précisément, les industriels, pour accroître la rapidité de conception, utilisent des méthodes et des outils, par exemple Matlab/Simulink, qui permettent à partir de description de haut niveau, appelées modèles, de générer automatiquement du code source. Une caractéristique intéressante de ces outils est de permettre la description, dans un même formalisme, de l'environnement physique et du programme informatique. De plus, grâce à des techniques de simulation, il est possible d’exécuter ces modèles afin de vérifier le comportement des systèmes ainsi modélisés. Ces outils sont alors le bon point de départ pour mettre en oeuvre des méthodes de vérification formelle.

La thèse intitulée "Analyse Statique de SysTèmes Hybrides décrits par des Modèles Exécutabes" a pour objectif de définir des méthodes de vérification formelle pour les modèles de programmes de contrôle-commande. Pour le moment les seules méthodes de vérification utilisées pour les programmes de contrôle-commande dans l'industrie se fondent sur la simulation numérique afin de garantir le bon fonctionnement de ceux-ci. Cependant, ces méthodes ne permettent pas de prouver, au sens mathématique, leur bon fonctionnement. Il s'agit par ce travail de faire un pas supplémentaire vers plus de sûreté des programmes de contrôle-commande en mettant au point des méthodes automatiques de vérification de bons comportements.

Travaux menés :
Les activités réalisées au cours de la première année de thèse ont eu pour objectif de s'approprier le sujet via une recherche bibliographique. L'insertion dans le domaine de la vérification formelle s'est appuyée sur l'Ecole de printemps DigiCosme (22-26 avril 2013). De plus, une introduction sur l'étude de systèmes hybrides a
été réalisée par une participation à EECI International Graduate School on Control (module M23 - Robust Hybrid Control Systems, 20-24 mai 2013).

La direction scientifique poursuivie en 2013 s'appuie sur l'analyse par intervalles pour résoudre le problème de calcul de certificats de barrière. Ces certificats sont une méthode qui permet de prouver qu'un système dynamique continu ne pourra pas atteindre une région interdite. Cela permet de faire des preuves de sûreté des systèmes à
temps continu. La mise en oeuvre de cette approche s'est traduite en un algorithme de résolution du problème de calcul de certificats de barrière.

Les actions de recherche menées en 2014 ont été, d'une part, de définir une méthode de calcul de fonctions barrières pour les systèmes dynamiques continus, et d'autre part, d'étendre ce premier travail pour les automates hybrides. Les deux solutions proposées s'appuient sur l'analyse par intervalle et, en particulier, sur la bibliothèque libre IBEX pour permettre à terme la diffusion des codes développés durant cette thèse. La concrétisation des ces travaux se traduit par une publication dans la conférence internationale CDC 2014 (Conference on Decision and Control) de la partie concernant des systèmes dynamiques continus.

Les actions de recherche pour l'année 2015 ont été concentrées sur la définition d'un algorithme de calculs de certificat de barrières pour les automates hybrides. La principale difficulté a été la gestion d'une exposition combinatoire des contraintes associées à la formulation des certificats de barrières sous la forme d'un problème de satisfaction de contraintes. Une approche incrémentale a été définie et une une première validation expérimentale a donné des résultats encourageants. La rédaction d'une version journal de l'article CDC sur le calcul des certificats de barrières pour les systèmes dynamiques continus a été également un élément important de l'activité. La publication dans le journal Automatica en 2017 est la concrétisation de cet effort.

L'année 2016 a été dédiée à la rédaction de thèse.

Soutenance

La thèse a été soutenue le 3 juillet 2017 à l'ENSTA ParisTech devant le jury formé de
  • M. Antoine Girard Directeur de Recherche au CNRS/L2S (Président du jury)
  • M. Nacim Ramdani Professeur des universités à l'Université d’Orléans (Rapporteur)
  • M. Stefan Ratschan Professeur à l'Académie tchèque des sciences (Rapporteur)
  • M. Nacim Meslem Maître de conférences à Grenoble INP (Examinateur)
  • M. Michel Kieffer Professeur des universités à l'Université Paris-Sud (Directeur de thèse)
  • M. Olivier Bouissou Ingénieur expert chez The Mathworks (Co-encadrant)
  • M. Alexandre Chapoutot Enseignant-Chercheur à l'ENSTA ParisTech (Co-encadrant)

Le manuscrit est accessible sur TEL

Perspectives :
La validation expérimentale plus poussée de l'algorithmes de calculs de certificats de barrières pour les systèmes dynamiques hybrides doit être conduite.
De nouvelles pistes de recherche sur le calcul d'invariant pour les systèmes dynamiques continus et hybrides grâce aux fonction barrières sont encore à mener.

Adel DJABALLAH
Image Adel Djaballah est originaire d'Algérie. Après son bac option scientifique, il suit des études d'informatique à l'Université des Sciences et de la Technologie HOUARI BOUMEDIENE d'Alger, obtenant d'abord une licence en informatique puis un Master en Génie Logiciel.
En 2011, il intègre le Master 2 recherche « Informatique : modélisation par le logiciel » de l'Université de Lorraine qu'il complète par un stage auprès du Centre d'Etudes de Populations, de Pauvreté et de Politiques Socio-Economiques (CEPS) au Luxembourg, pour lequel il développe un outil d’aide à la décision pour l’optimisation d'un réseau de transport.

En 2012, il commence sa thèse « Vérification formelle de systèmes hybrides » à l'ENSTA ParisTech, sous la direction d'Alexandre CHAPOUTOT, Olivier BOUISSOU et Michel KIEFFER.