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

  1. La gestion logistique des entrepôts pour des tiers 
  2. 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