Image pour le projet MALTHY
LinkedIn Google Plus Twitter Email

Le projet MALTHY

Méthodes ALgébriques pour la vérification de modèles Temporisés et Hybrides
Des systèmes informatiques complexes sont désormais embarqués dans presque toutes les machines que nous utilisons quotidiennement pour nous déplacer (voiture, trains, avions), pour travailler ou pour communiquer (téléphones portables). Actuellement, ces systèmes sont toujours conçus puis validés par des simulations et des tests qui ne permettent pas de garantir rigoureusement leur fiabilité, notamment lorsqu'ils opèrent dans un environnement changeant et incertain. Des méthodes de validation rigoureuses, capables de tenir compte de cet environnement, sont nécessaires.

Le model-checking est une technique utilisée depuis plus de 20 ans pour déterminer automatiquement si une propriété donnée est satisfaite par toutes les exécutions d'un système. Cette technique demande de modéliser formellement le système embarqué et son environnement, sous forme d'un système hybride. Un système hybride est un cadre mathématique rigoureux qui combine plusieurs dynamiques (discret/continu, logique/numérique). Le model-checking des systèmes hybrides est un problème généralement indécidable pour toute propriété non-triviale, ce qui nous contraint à calculer des approximations des états atteignables pour valider des propriétés de sûreté ou de vivacité.

Les limites pratiques de cette technique, en termes de temps de calcul et de consommation mémoire, se font sentir quand on tente de vérifier les systèmes embarqués complexes. Un facteur crucial pour dépasser ces limites est de disposer de bonnes structures de données et d'algorithmes capables de modéliser et de valider efficacement les systèmes temporisés et hybrides.

Le but de ce projet de recherche est de faire progresser l'état de l'art du model-checking des systèmes temporisés et hybrides en appliquant des méthodes avancées et des outils issus des sciences mathématiques: algèbre linéaire et géométrie algébrique. Ces méthodes et outils incluent de nouvelles structures de données comme les polyèdres tropicaux, les fonctions support et les zonotopes, et de nouveaux algorithmes comme l'itération sur les politiques et la programmation conique.

Pour atteindre ce but, ce projet propose de développer trois types de méthodes algébriques pour la vérification des systèmes temporisés et hybrides:

  • les méthodes tropicales, pour traiter efficacement des invariants disjonctifs qui surviennent en model checking, en particulier de systèmes temporisés;
  • les domaines abstraits sous-polyédriques, pour accroître fortement l’efficacité de model checking des systèmes hybrides
  • les méthodes semi-algébriques convexes, pour obtenir des représentations d'ensembles encore plus expressives en vue des analyses plus précises des systèmes hybrides. 

MALTHY est soutenu par le programme ANR INS 2013 (Ingénierie Numérique et Sécurité) pour un montant de 918 776 euros. C’est un projet de 48 mois qui a débuté en janvier 2014.

Les partenaires de MALTHY

  • CEA-LIST Saclay
  • INRIA Saclay
  • IRISA/INRIA Rennes
  • VERIMAG Grenoble (coordinateur)
  • VISEO

Pour plus d’informations :

Porteur de l’Offre
Frédérique SEGOND

Titulaire d'un doctorat en mathématiques appliquées de l'Ecole des Hautes Etudes en Sciences Sociales Frédérique SEGOND rejoint VISEO en 2011.

Frédérique a travaillé pendant 18 ans au Centre européen de recherche de Xerox à Grenoble, France. En 2003, elle est Principal Scientist & Area Manager du groupe de recherche Parsing & Semantics spécialisé dans l’analyse de documents textuels.

Tout au long de sa carrière de chercheuse elle a défini, travaillé et dirigé une vingtaine de projets de recherche collaboratifs tels qu’ALADIN, Europeanna, Galateas et CACAO. Elle a également travaillé au centre scientifique d’IBM France et au centre de recherche d’IBM Watson à Yorktown où elle a étudié les liens entre syntaxe et sémantique.

Frédérique est co-auteur de six ouvrages, de plus de 50 articles scientifiques et de 5 brevets. Elle fait partie du comité de pilotage CONTINT à l'Agence Nationale pour la Recherche (ANR), présidente de l'Association pour le Traitement Automatique des Langues (ATALA), membre du Conseil d’administration d’ELRA (European Language Resources Association), membre du conseil d'administration de l'Université Stendhal, et fournit également son expertise scientifique à la Commission européenne.

Publications et Brevets

Curriculum Vitae