Travaux de fin d'études: Année académique 2003-2004
Informatique
P. Wolper
Utilisation des algorithmes de satisfaisabilité en vérification
de programmes
Pour augmenter la fiabilité des programmes, et en particulier les
applications critiques dans les systèmes enfouis, il est utile d'analyser
de façon systématique leurs comportements possibles, c'est-à-dire
de "vérifier" les programmes. Cela se fait le plus souvent à
l'aide d'une exploration de l'espace des états du programme, à
la recherche de comportements incorrects. Une tendance qui se développe
depuis quelques années est de d'effectuer cette recherche de comportements
incorrects à l'aide d'algorithmes vérifiant la satisfaisabilité
de formules de la logique propositionnelle. Un article
récent développe des techniques qui étendent de façon
très substantielle les possibilités de ce type d'approche.
Le but de ce mémoire est de faire le point sur l'utilisation des techniques
de satisfaisabilité en vérification de programmes et de tenter
d'utiliser ce type d'approche dans le cadre de logiques plus expressives
que la logique propositionnelle, en particulier la théorie de l'arithmétique
sans multiplication (arithmétique de Presburger)
Personne à contacter: P. Wolper
La simplification des programmes en vue de leur vérification
Les méthodes d'analyse des programmes par exploration de l'espace
des états se heurtent fréquemment au caractère infini,
ou fini et très grand, de cet espace. Une possibilité pour limiter
l'impact de cette difficulté est de simplifier les programmes avant
de procéder à l'exploration de l'espace des états. Cette
simplification prend le plus souvent la forme d'une "abstraction" qui restreint
l'espace des états du programme tout en préservant les caractéristiques
essentielles de son comportement. Il existe une variété d'abstractions
possibles, mais une particulièrement adaptée est celle basée
sur le concept de "data-independence" qui exploite le fait que les valeurs
de certaines données sont en fait sans influence sur le comportement
du programme. Cette situation est, par exemple, fréquente dans les
protocoles de communication ou la majeure partie des données traitées
sont simplement transmises sans modification.
Le but de ce mémoire est d'abord de faire le point sur les
techniques d'abstraction et, en particulier, sur l'interaction entre ces
techniques et les techniques de vérification les plus récentes.
Ensuite, des combinaisons de techniques de vérification et d'abstraction
seront étudiées et évaluées sur des études
de cas.
Personne à contacter: A. Legay
La vérification des programmes booléens
Une des difficultés majeures de la vérification
de programmes par exploration de leur espace d'états est que le nombre
d'états à considérer est souvent extrêmement
grand, voire infini. En effet, quelques variables entières de 32
bits suffisent pour que le système ait un nombre tout à fait
astronomique d'états. Pour vérifier un programme il est donc
souvent nécessaire d'en construire une version simplifiée,
parfois aussi appelée abstraite, où les données utilisées
sont restreinte à un nombre limité de valeurs. Une technique
de simplification possible est de remplacer toute variable par une variable
booléenne. Cela limite radicalement la croissance du nombre d'états
liée aux variables et simplifie la vérification qui, même
pour un programme Booléen est loin d'être triviale, notamment
ne présence de procédures récursives. L'utilisation
de programme booléens comme abstractions auxquelles on applique la
vérification pose deux questions importantes. La première est
celle des techniques utilisables pour la vérification des programmes
Booléens. La deuxième est celle de la signification de la vérification
réalisée sur le programme booléen par rapport au programme
non simplifié de départ. Une série de travaux se sont
récemment intéressés à ces questions (voir par
exemple le projet SLAM).
La but de ce mémoire est de faire le point sur la question, d'évaluer
les méthodes existantes et, d'en tester l'applicabilité.
Personne à contacter: P. Wolper
Travaux proposés par la firme Watermark
- La gestion logistique des entrepôts
pour des tiers
- Définition et développement
d'une solution verticale pour les entreprises de construction et génie-civil
Informations sur l'environnement
utilisé et références
de la firme Watermark.
Pour ces travail, contacter Monsieur Guy Timmermans (gtimmermans@watermark-europe.com,
Tel: 04 254 49 00)
de Watermark et informer P. Wolper
Pierre Wolper
Wed Jul 30 12:11:46 CEST 2003