Méthodes ALgèbriques pour la vérification de modèles Temporisés et HYbrides – MALTHY

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 terme 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 domains 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.

Les structures de données et les algorithmes résultant de l'étude de ces méthodes seront utilisés pour améliorer des logiciels (pyECDAR, HybridFluctuat et SpaceEx) et des bibliothèques (APRON).

Un autre objectif important de ce projet est de démontrer que le model checking des systèmes temporisés et hybrides peuvent être exportés vers l'industrie et contribuer à la conception de confiance des systèmes embarqués critiques. Nous appliquerons ces nouvelles techniques à la vérification automatique de matériel médical, au travers une études de cas industrielle de pompes à injection, fournie par le partenaire Object Direct.