Peter Schrammel - Méthodes logico-numériques pour la vérification des systèmes discrets et hybrides

12:00
Jeudi
18
Oct
2012
Organisé par : 

Peter Schrammel

Intervenant : 

Peter Schrammel

Jury : 
— Laurent Fribourg, DR CNRS, LSV Cachan, Rapporteur 
— Éric Goubault, DR CEA, LIST Saclay, Rapporteur 
— Laure Danthony-Gonnord, Maître de Conférences, LIFL Lille, Examinatrice 
— Jérôme Leroux, CR CNRS, LaBRI Bordeaux, Examinateur 
— Marc Pouzet, Professeur ENS Paris, LIENS Paris, Examinateur 
— Alain Girault, DR INRIA, LIG Grenoble, Directeur de thèse 
— Bertrand Jeannet, CR INRIA, LIG Grenoble, Co-Directeur de thèse

Cette thèse étudie la vérification automatique de propriétés de sûreté de systèmes logico-numériques discrets ou hybrides. Ce sont des systèmes ayant des variables booléennes et numériques et des comportements discrets et continus. Notre approche est fondée sur l’analyse statique par interprétation abstraite.

Nous adressons les problèmes suivants : les méthodes d’interprétation abstraite numériques exigent l’énumération des états booléens, et par conséquent, ils souffrent du problème d’explosion d’espace d’états. En outre, il y a une perte de précision due à l’utilisation d’un opérateur d’élargissement afin de garantir la terminaison de l’analyse. Par ailleurs, nous voulons rendre les méthodes d’interprétation abstraite accessibles à des langages de simulation hybrides.

Dans cette thèse, nous généralisons d’abord l’accélération abstraite, une méthode qui améliore la précision des invariants numériques inférés. Ensuite, nous montrons comment étendre l’accélération abstraite et l’itération de max-stratégies à des programmes logico-numériques, ce qui aide à améliorer le compromis entre l’efficacité et la précision. En ce qui concerne les systèmes hybrides, nous traduisons le langage de programmation synchrone et hybride Zelus vers les automates hybrides logico-numériques, et nous étendons les méthodes d’analyse logico-numérique aux systèmes hybrides. Enfin, nous avons mis en oeuvre les méthodes proposées dans un outil nommé ReaVer et nous fournissons des résultats expérimentaux.

En conclusion, cette thèse propose une approche unifiée à la vérification de systèmes logico-numériques discrets et hybrides fondée sur l’interprétation abstraite qui est capable d’intégrer des méthodes d’interprétation abstraite numériques sophistiquées tout en améliorant le compromis entre l’efficacité et la précision.