Site menu:



Quatre orateurs invités à MSR2019

Béatrice Bérard
LIP6 - CNRS UMR 7606, France

Biographie de l'orateur ... Biographie de l'orateur


Titulaire d’un doctorat et d’une HDR de l’université Paris 7, Béatrice Bérard a successivement exercé comme maître de conférences à l’Université de Caen et à l’Ecole Normale Supérieure de Cachan, puis comme professeur à l’Université Paris-Dauphine et à Sorbonne Université. Ses thèmes de recherche sont centrés sur la modélisation et l’analyse de systèmes complexes, dans lesquels plusieurs caractéristiques peuvent être combinées : les contraintes quantitatives liées au temps ou au probabilités, les interactions avec un environnement parfois hostile et la répartition sur plusieurs sites. Outre l’étude des systèmes hybrides, ses travaux les plus récents abordent les questions de sécurité, notamment via les propriétés d’opacité, et la synthèse de contrôleurs, avec des applications aux essaims de robots et aux systèmes de transport automatisés.



Flots d’information, opacité — et quelques remarques sur le diagnostic


Résumé de l'exposé   : Dès les années 80, Goguen et Meseguer s’intéressent aux propriétés de sécurité et aux modèles associés, en définissant notamment la « non interference » : sur toute séquence d’entrées, un utilisateur non autorisé doit observer le même résultat, que les actions d’un utilisateur de haut niveau soient ou non supprimées de cette séquence. Par la suite, de nombreux formalismes et techniques ont été proposés pour décrire et vérifier des propriétés de ce type. Je présenterai quelques résultats de ces dernières années, concernant des aspects qualitatifs et quantitatifs, avec des attaquants actifs ou passifs, à partir de travaux réalisés avec plusieurs collègues.

Antoine Girard
Laboratoire des Signaux et Systèmes (L2S) - CNRS, France

Biographie de l'orateur ... Biographie de l'orateur


Antoine Girard est directeur de recherche au CNRS et membre du Laboratoire des Signaux et Systèmes (L2S). Il a reçu le doctorat en mathématiques appliquées de Grenoble INP en 2004. De 2004 à 2006, il était chercheur post-doctorant à University of Pennsylvania et à l’Université Grenoble-Alpes. De 2006 à 2015, il était maître de conférences à l'Université Grenoble-Alpes. Ses travaux de recherche portent principalement sur l'analyse et le contrôle de systèmes hybrides, en mettant l'accent sur les approches numériques, les méthodes formelles et les applications aux systèmes cyber-physiques. Antoine Girard a reçu le prix George S. Axelby Outstanding Paper Award de l'IEEE Control Systems Society en 2009. En 2014, il a reçu la médaille de bronze du CNRS. En 2015, il a été nommé membre junior de l'Institut Universitaire de France (IUF). En 2016, il a reçu une bourse ERC Consolidator Grant. En 2018, il a reçu le premier Test of Time Award de la conférence Hybrid Systems: Computation and Control et le European Control Award, décerné par la European Control Association.



Contrôle symbolique pour la programmation des systèmes cyber-physiques



Résumé de l'exposé   : Véhicules autonomes, bâtiments intelligents ou robots promettent de transformer le quotidien de notre société dans toutes ses dimensions (transport, logement, industrie, santé, assistance aux personnes âgées ...). Ces systèmes sont des exemples de systèmes cyber-physiques (CPS) résultant de l'intégration de composants informatiques et de processus physiques. Le développement de ces systèmes est souvent complexe (en raison d'interactions cyber-physiques) et comporte des exigences de sécurité critiques. Dans cet exposé, je présenterai les prémisses d'un cadre de programmation des CPS permettant un développement rapide et sûr de leurs fonctionnalités via un langage de programmation de haut niveau. L'originalité de l'approche consiste à considérer que les programmes ne sont pas destinés à être exécutés sur la plate-forme numérique formée de composants informatiques, mais sur la plate-forme cyber-physique, qui comprend en outre la partie physique du système. Ainsi, les programmes de haut niveau ne spécifient pas le comportement des composants informatiques mais directement celui du système cyber-physique. Ensuite, un outil de synthèse automatique utilise un modèle du processus physique pour générer des algorithmes de contrôle de bas niveau mettant en oeuvre le comportement spécifié. Je commencerai mon exposé en introduisant un langage de haut niveau pour CPS, directement inspiré du formalisme des automates hybrides. Suivant le paradigme de "synthèse correcte par construction", les algorithmes de contrôle de bas niveau sont synthétisés par des techniques de contrôle symbolique. Le concept clé du contrôle symbolique est celui du modèle symbolique, qui est un système dynamique à états finis, obtenu par l'abstraction de trajectoires physiques sur un ensemble fini de symboles. Lorsque les dynamiques symboliques et physiques sont formellement liées par une relation comportementale (par exemple, une simulation ou une bisimulation), les contrôleurs synthétisés pour le modèle symbolique à l'aide de techniques de synthèse discrète peuvent être affinés pour devenir des contrôleurs certifiés pour le système physique. Nous terminerons l’exposé par quelques illustrations dans le domaine des véhicules autonomes.

Laurent Fribourg
Laboratoire Spécification et Vérification (LSV) - CNRS, ENS Paris-Saclay

Biographie de l'orateur ... Biographie de l'orateur


Laurent Fribourg est directeur de recherche au CNRS. Il travaille au LSV à l’ENS Paris-Saclay, laboratoire dont il est membre fondateur et qu’il a dirigé de 2011 à 2015. Il est depuis 2018 directeur de l’Institut Farman qui fédère et anime les travaux de cinq laboratoires de recherche de l'ENS Paris-Saclay (CMLA, LMT, LSV, LURPA, SATIE) dans le domaine de la modélisation, simulation et validation des systèmes complexes.



Quelques applications des constantes de Lipschitz unilatérales



Résumé de l'exposé   : Les constantes de Lipschitz unilatérales (OSL) ou "normes logarithmiques" ont été introduites indépendamment en 1958 par Dahlquist et Lozinskii afin d'obtenir des bornes d’erreur fines sur les résultats d'algorithmes d’intégration de systèmes d’équations différentielles ordinaires (ODE). Nous verrons que l'OSL traduit une notion de "stabilité locale" qui s’exprime également en terme de valeurs propres de matrice jacobienne, de taux de contraction de champ de vecteurs ou d’exposant de Lyapunov. Nous expliquerons ensuite comment, pour certaines classe d’ODE paramétrées, on peut analytiquement décomposer le plan de phase en un sous-domaine d’OSL positif et un sous-domaine d’OSL negatif, puis comment exploiter cette décomposition pour prouver formellement la structure de cycles limites et l'existence de points de bifurcations.

Amar Bouali
Amar Bouali, responsable du centre de référence de l’IDEX UCA JEDI "Défis du numérique" et chercheur Inria, France

Biographie de l'orateur ... Biographie de l'orateur


Amar Bouali est directeur du Centre « Défis du numérique » de l’Université Côte d’Azur depuis mai 2017, en charge du développement de partenariats entre la recherche publique et les entreprises en matière d’innovation, de transfert de technologie et de création d’entreprise. Amar est également Directeur de la plateforme InriaTech d’Inria dédié au transfert. Avant de rejoindre l’Université Côte d’Azur, Amar a passé 16 ans chez Esterel Technologies, éditeur de logiciels, développant des environnements d’ingénierie pour la conception de logiciels critiques en temps réel, axés sur des secteurs tels que l’aéronautique, les transports, l’énergie et le secteur médical. En 2012, la société a été rachetée par Ansys, leader mondial de la simulation numérique. Amar a débuté dans cette société en tant qu'ingénieur senior R&D pendant 2 ans; Il a ensuite occupé la direction technique des avant-ventes pendant 7 ans, finissant les 7 dernières années en tant que vice-président des opérations, gérant les ventes sur les territoires de l'Europe du Sud, de la Turquie, du Moyen-Orient et de l'Afrique. Amar a commencé sa carrière professionnelle en tant que chercheur scientifique à Inria Sophia Antipolis, où il a accumulé 10 années d’expérience, en commençant par l’obtention d'un doctorat en informatique de l'Université de Paris 7 en 1993 au sein d'une équipe de recherche commune à Inria Sophia Antipolis et au Centre de mathématiques appliquées de Mines ParisTech.



De l'usage de méthodes formelles et basées modèles dans l'industrie des systèmes embarqués critiques



Résumé de l'exposé   : Les industries des systèmes embarqués critiques, telles que l'aéronautique, le ferroviaire, le nucléaire ont orienté leurs activités de recherche et de développement vers l'usage de méthodes formelles et basées modèles. On présente tout d'abord les défis que posent l'augmentation croissante de la complexités des systèmes développés dans ces industries, intrinsèquement réactifs et temps-réels. On présente ensuite comment les approches basées modèles et formelles apportent des solutions pour relever ces défis. Enfin, la présentation fait part de retour d'expérience d'une solution industrielle fondée sur des travaux de recherche et de technologies de laboratoires essentiellement français, proposant de telle approches pour les ingénieries systèmes et logicielles. On fait part des avantages apportés par ce type de solution et on invite à réfléchir sur l’adoption de telles approches pour les autres secteurs industrielles, ou la complexité des systèmes logiciels est grandissante et où le caractère critique du bon fonction devient prépondérant, notamment en matière de sécurité.