Proposition de sujet de thèse par Rueher Michel

ED STIC - Proposition de Sujets de Thèse
pour la campagne d'Allocation de thèses 2014
Axe Sophi@Stic :
aucun|
Titre du sujet :
Localisation d'erreurs dans un système de contraintes sur les flottants
Mention de thèse :
Informatique
HDR Directeur de
thèse inscrit à l'ED
STIC :
Rueher Michel
Co-encadrant de thèse éventuel :
Nom :
Collavizza
Prénom :
Hélène
Email :
[email protected]
Téléphone :
0492965163
Email de contact
pour ce sujet :
[email protected]
Laboratoire
d'accueil :
I3S
Description du sujet :
Contexte applicatif:
Les programmes embarqués sont de plus en plus utilisés dans des systèmes critiques (e.g. ABS
sur les voitures). La sûreté de fonctionnement repose donc sur l’exécution
correcte du code. Ces codes font appel à de nombreux calculs arithmétiques et notamment à des
calculs effectués à l'aide des nombres flottants. Cette thèse s'inscrit dans un
projet qui vise à développer des méthodes et techniques pour renforcer la fiabilité de tels
programmes.
Le calcul sur les flottants introduit des risques supplémentaires au niveau de ces programmes. En
effet, leur spécification est en général écrite par un utilisateur qui raisonne sur
des nombres réels alors que les résultats du calcul sur les nombres flottants peuvent être
sensiblement différents du fait des problèmes liés aux arrondis (cancellation,
Page 1/3
absorption, …). Il peut en résulter une plus grande instabilité des programmes[19], c’est-à-dire
que les décisions prises par le programme sur la base de calculs sur flottants
peuvent être totalement différentes de celles qui auraient été prises sur la base d'un calcul sur
les réels. Dans la pratique, un calcul sur les réels n'est en général pas possible
ou trop coûteux (par exemple si on utilise une précision suffisante pour éviter tout problème
d'arrondi).
L'analyse statique et l'interprétation abstraite (IA) ont été largement utilisées pour détecter des
erreurs dans des programmes avec des nombres flottants [17,18]. Une des
limites de l'IA réside dans les fausses alarmes dues aux sur-approximations; c'est à dire des
erreurs qui ne peuvent pas se produire dans le contexte de calcul effectif, mais
uniquement au niveau de son approximation. La combinaison de l'IA et des techniques CSP [1,5]
permet non seulement de calculer de telles approximations mais aussi de
générer des contre-exemples qui violent certaines propriétés [20,21]; contre-exemples qui
peuvent aussi être générés à l'aide de solveurs comme CBMC
(http://www.cprover.org/cbmc/),
Z3
(http://z3.codeplex.com/)
et
MathSAT
(http://mathsat.fbk.eu/). Toutefois, dans tous les cas de figure, un problème majeur réside dans la
localisation des erreurs. Ce problème est équivalent à celui de l'identification dans l'ensemble des
contraintes associées au programme et aux contre-exemples d'un sous
ensemble de contraintes "pertinent.
Sujet proposé:
L'objectif du travail proposé est de faciliter la localisation d'erreurs dans un système de
contraintes sur les flottants. Dans le cadre de cette thèse, on va rechercher des
algorithmes incrémentaux raisonnablement efficaces pour des systèmes de contraintes hybrides
comprenant des entiers, des booléens et des nombres flottants. Plus
précisément, on s'intéressera au calcul d'un sous-ensemble pertinent de contraintes pour
faciliter la localisation des erreurs dans un système de contraintes hybrides. Ce
problème a fait l'objet de nombreux travaux, en particulier en recherche opérationnelle et en
programmation par contraintes où la mise au point d'un système de contraintes est
un problème critique. Un des objectifs sera donc de réutiliser et d'adapter au contexte des
nombres flottants les travaux effectués pour des systèmes LP (linear programming),
MIP (mixed integer programming), CSP ou SAT.
Lorsqu’on recherche des informations utiles pour la localisation des erreurs sur les systèmes de
contraintes numériques, on peut s’intéresser à deux types d’informations :
1.Combien de contraintes dans un ensemble de contraintes insatisfiables peuvent être
satisfaites ?
2.Où se situe le problème dans le système de contraintes ?
Pour répondre à ces questions plus formellement, on peut utiliser les notions de MUS, MSS et
MCS introduites dans [22].
Différents algorithmes ont été proposés pour le calcul des IIS/MUS et MCS. Parmi les premiers
Page 2/3
travaux, ont peut mentionner les algorithmes Deletion Filter, Additive Method,
Additive Deletion Method, Elastic Filter qui on tété développés dans la communauté de recherche
opérationnelle [14]. Les trois premiers algorithmes sont des algorithmes
itératifs alors que le quatrième utilise des variables d’écart pour identifier dans la première phase
du Simplexe les contraintes susceptibles de figurer dans un IIS. Junker [15] a
proposé un algorithme générique basé sur une stratégie ”Divide-and-Conquer” pour calculer
efficacement les IIS/MUS lorsque la taille des sous-ensembles conflictuels est
beaucoup plus petite que celle de l’ensemble total des contraintes. L’algorithme de Liffiton et
Sakallah [24] qui calcule d’abord l’ensemble des MCS par ordre de taille croissante,
puis l’ensemble des MUS est basé sur la propriété mentionnée ci-dessus. Cet algorithme, que
nous avons utilisé dans notre implémentation est décrit dans la section suivante.
Plusieurs améliorations [23, 26] de ces algorithmes on été proposées ces dernières années mais
elles sont assez étroitement liées à SAT et a priori assez difficilement
transposables dans un contexte où nous avons de nombreuses contraintes numériques sur les
flottants.
La difficulté majeure pour l'adaptation de ces algorithmes aux flottants vient du fait de la
pauvreté de la sémantique de l'arithmétique sur les flottants.
Références et sujet étendu : http://users.polytech.unice.fr/~rueher/sujet_CR_2014.pdf
URL : http://users.polytech.unice.fr/~rueher/sujet_CR_2014.pdf
English version:
Page 3/3

Download Report