Validation inductive de programmes et de systèmes hybrides

Enseignant : Sylvie Putot

Cours :

L’analyse statique de programmes consiste à vérifier statiquement (i.e. sans les exécuter) des propriétés dynamiques (à l’exécution) des programmes. Les classes de propriétés à vérifier sont très diverses comme la sûreté (par exemple l’absence d’erreurs à l’exécution), la vivacité (par exemple la garantie de réponse à un signal donné), la sécurité (par exemple la confidentialité d’informations traitées par un programme), etc. La grande difficulté pour démontrer automatiquement ces propriétés dynamiques réside dans le fait de trouver les bons arguments inductifs nécessaires pour en faire la preuve. Diverses solutions sont possibles : le demander à l’utilisateur (méthodes déductives), se restreindre à un modèle fini (vérification exhaustive) ou calculer l’argument inductif par approximation de la sémantique du programme (via des techniques d’approximation de point fixe de l’interprétation abstraite). Le cours explore cette dernière technique. La validation des systèmes embarqués critiques en constitue une application naturelle. Une difficulté qui apparait rapidement dans ce cadre est la nécessité de prendre en compte l’interaction du système avec son environnement physique. Les systèmes à valider sont alors hybrides, c’est-à-dire couplent des composantes discrètes et continues. Nous concluerons le cours par une ouverture sur la modélisation et l’analyse de tels systèmes.

TD : 10.5 heures de TD pour 10.5 heures de cours.

Prérequis :