Habilitation day: September 19th 2016

Talks

HDR Xavier Thirioux: Verifying Embedded Systems

Jury

Reviewers :

Matthieu Martel Professeur à l’Université de Perpignan Via Domitia, LAMPS
Marc Pouzet Professeur à l’Université Pierre et Marie Curie, ENS, département d’informatique, équipe PARKAS
Sylvain Conchon Professeur à l’Université Paris-Sud, LRI, équipe Toccata

Members:

Virginie Wiels Directrice du DTIM, ONERA Toulouse
Éric Féron Professor of Aerospace Engineering at Georgia Tech, USA
Didier Henrion Directeur de recherches au LAAS-CNRS, Université de Toulouse
Robert De Simone Directeur de Recherche INRIA Sophia-Antipolis, équipe AOSTE
Philippe Queinnec Professeur à l’INPT/IRIT

Manuscript

  • Xavier Thirioux: Verifying Embedded Systems [pdf]

Résumé

Mes thématiques de recherche concernent la vérification automatique de code produit par un générateur de code, avec un cadre d'application s'orientant plus particulièrement vers les systèmes embarqués critiques. Une première approche est de permettre la production d'un code correct par construction à partir d'une spécification formelle. Dans un cadre d'ingénierie des modèles, on souhaite fiabiliser et maîtriser la production et la transformation de modèles à travers l'application d'opérations les plus générales et utiles possibles, opérations qui seront définies et implantées correctes grâce à un assistant de preuve comme Coq.
Une seconde approche cherche, dans une optique de génération de code standard, i.e. détachée de sa spécification, à combler le fossé entre un code de bas niveau et une spécification fonctionnelle de haut niveau, fossé qui rend les preuves de correction diffciles. On propose une combinaison de plusieurs techniques : la génération de code et de sa preuve de correction (sous forme d'assertions à vérifier) conjointement, appelée proof carrying code d'une part ; l'utilisation de méthodes à base de relations de rafinement d'autre part. Ceci permet par exemple, dans le cadre des systèmes critiques embarqués, de valider complètement et automatiquement la correction de codes produits par des générateurs permettant des optimisations agressives, contrairement aux usages où ces optimisations sont habituellement bannies.
Les perspectives de recherche s'articulent en 3 parties. Premièrement, en s'appuyant sur les travaux réalisés autour de la formalisation en Coq de l'ingénierie des modèles, étudier les meilleures façons de prolonger et approfondir le cadre défini pour supporter plus d'opérations, et permettre notamment le traitement de la sémantique dynamique des modèles, i.e. les propriétés liées à leurs exécutions, ce qui constitue jusqu'à maintenant un verrou majeur qui n'a donné lieu qu'à des solutions partielles. Ceci passe certainement par une approche basée sur les principes de la théorie des catégories.
Deuxièmement, développer les techniques et promouvoir la chaîne d'outils qui les implantent, permettant la vérification automatique de code source Lustre, à travers le support de constructions de plus en plus complexes des dernières versions du langage utilisées dans l'industrie, tout en travaillant sur l'efficacité des procédures de vérification et le guidage éventuel des heuristiques utilisées dans la recherche et la construction des preuves, qui est un domaine relativement inexploré.
Troisièmement, s'orienter vers des spécifications fonctionnelles représentant des propriétés numériques, i.e. étudier les programmes comme des systèmes dynamiques, notamment dans les systèmes embarqués. Des premiers résultats encourageants ont d'ores et déjà été obtenus sur des systèmes à dynamique polynomiale à travers des collaborations avec le LAAS. Les autres dynamiques plus complexes pourraient alors, par un calcul d'une approximation en série de Taylor avec bornes d'erreur exactes, se ramener au cas polynomial et donner lieu à une véritable avancée dans la vérification de code numérique complexe. Enfin, l'ensemble des contributions sont et seront déclinées dans des méthodes et implantées dans des outils intégrés dans des ateliers ou des démonstrateurs.

HDR Pierre-Loïc Garoche: Convex Optimization-based Static Analysis for Control Systems

Jury

Reviewers:

Éric Goubault Professeur au LIX à l’École Polytechnique
Ilya Kolmanovsky Professor of Aerospace Engineering at Michigan University, USA
David Monniaux Directeur de recherches au CNRS, Laboratoire Vérimag

Members:

Behçet Açikmeşe Associate Professor of Aeronautics & Astronautics at University of Washington, USA
Éric Féron Professor of Aerospace Engineering at Georgia Tech, USA
John Hauser Associate Professor, Dept. of Electrical and Computer Engineering at University of Colorado Boulder, USA
Didier Henrion Directeur de recherches au LAAS-CNRS, Université de Toulouse
Matthieu Martel Professeur à l’Université de Perpignan Via Domitia, Laboratoire de Mathématiques et de Physique (LAMPS)
Philippe Queinnec Professeur à l’INPT/IRIT, Université de Toulouse

Manuscript

Résumé

Ces travaux s’intéressent spécifiquement à la vérification d’implantation d’algorithmes de contrôle comme ceux utilisés dans les avions civils. Ces contrôleurs sont essentiellement conçus en combinant des contrôleurs simples (linéaires par morceaux) avec des logiques de détection de fautes et de reconfiguration. L’analyse statique de ces systèmes est aujourd’hui difficile car les propriétés invariantes de ces contrôleurs sont souvent super-linéaires, par exemple quadratiques, alors que les méthodes de calcul d’invariants par interprétation abstraite ou de preuve automatique avec des solveurs de satisfiabilité (SMT) traitent assez mal les systèmes ou propriétés non linéaires.
Les travaux présentés, inspirés des méthodes utilisés en analyse temporelle dans le monde du contrôle, reposent sur la formulation de ces problèmes et leur résolution comme des problèmes d’optimisation convexe dans le cone des matrices définies positives (programmation SDP avec des inégalités linéaires de matrices (LMI) ou polynômes somme de carrés). Ces approches permettent de synthétiser automatiquement des invariants quadratiques ou polynomiaux, capables de capturer le comportenent de ces implantations de contrôleurs. Les méthodes proposées s’appliquent tant au niveau modèle qu’au code, et traitent spécifiquement des problématiques liées à l’utilisation d’arithmétique en virgule flottante.
Les perspectives de ces travaux concernent essentiellement la vérification d’implantation d’algorithmes numériques em- barqués. L’ambition est de traiter plus de propriétés et plus de systèmes. Plus de propriétés signifie, tant au niveau des modèles que du code, d’exprimer formellement et de vérifier automati- quement des propriétés systèmes plus intéressantes que le simple comportement borné du système. Pour les algorithmes de contrôle il s’agit des propriétés de stabilité, robustesse et performance (overshoot, time to settle, etc). Pour d’autres types d’algorithmes, il s’agira de bornes sur le temps de convergence, ou la garantie de satisfaire certaines contraintes sur la solution calculée. Plus de systèmes signifie la volonté de traiter plus que de simple contrôleurs linéaires. Je souhaite développer des ana- lyses capables de traiter des systèmes simples mais réalistes (LPV, interpolation linéaire de contrôleurs, ...) aux fonctions numériques plus avancées comme utilisée dans des algorithmes de calcul de trajectoire pour l’anti-collision ou l’atterissage planétaire. L’ensemble des méthodes et outils développés seront intégrés dans des ateliers et démonstrateurs open-source applicables sur des systèmes de taille significative.

Author: Pierre-Loïc Garoche

Created: 2016-07-29 Fri 17:15

Emacs 24.5.1 (Org mode 8.2.10)

Validate