Soutenance de thèse
Arnaud Sangnier
Titre de la thèse
Vérification de systèmes avec compteurs et pointeurs.
Date et lieu
Le
Vendredi 21 Novembre 2008 à Cachan à 14h00.
Salle de Conférences, Pavillon des Jardins, École Normale Supérieure
de Cachan.
Plan d'accès
Composition du jury
Résumé de la thèse
Au cours des dernières années, les méthodes formelles se sont avérées être une approche prometteuse pour garantir que le comportement d'un système informatique respecte une spécification donnée. Parmi les diffèrentes techniques développées, le model-checking a été récemment étudié et appliqué avec succès à un grand nombre de modèles comme les systèmes à compteurs, les automates communicants (avec perte), les automates à pile, les automates temporisés, etc. Dans cette thèse, nous considérons deux modèles particuliers dans l'objectif de vérifier des programmes manipulant des variables entières et des variables de pointeurs. Dans une première partie, nous nous intéressons aux systèmes à compteurs. Nous commençons par définir ce modèle ainsi que ses diffèrentes restrictions. Nous introduisons ensuite une sous-classe de systèmes à compteurs, appelée les machines à compteurs reversal-bornées, pour lesquelles de nombreux problèmes d'accessibilité sont décidables. Nous montrons que cette classe peut être étendue tout en gardant les résultats de décidabilité et nous prouvons qu'il est possible de décider si un Système d'Addition de Vecteurs avec états est reversal-borné, alors que cela n'est pas possible si l'on considère les systèmes à compteurs dans leur généralité. Nous finissons cette partie sur les systèmes à compteurs par l'étude de problèmes de model-checking de logiques temporelles. Les logiques temporelles que nous prenons en compte permettent de parler des données manipulées par le système. En particulier, nous montrons que le model-checking d'automates à un compteur déterministes avec des formules de la logique LTL avec registres est décidable, mais que cela n'est plus vrai lorsque l'hypothèse sur le déterminisme est supprimée. Dans une deuxième partie, nous introduisons le modèle des systèmes à pointeurs, qui est utilisé pour représenter des programmes manipulant des listes simplement chaînées. Nous donnons un algorithme qui traduit tout système à pointeurs en un système à compteurs qui lui est bisimilaire. Ceci nous permet de réutiliser les méthodes existantes pour l'analyse de systèmes à compteurs pour vérifier des programmes avec listes. Nous présentons ensuite une extension de la logique CTL* pour vérifier des propriétés temporelles sur de tels programmes, et nous étudions la décidabilité du problème de model-checking pour cette nouvelle logique. Finalement, dans une dernière partie, nous donnons une description de l'outil TOPICS (Translation of Programs Into Counter Systems) qui traduit un programme écrit dans un fragment syntaxique du langage C en un système à compteurs.
Mots-Clefs
Vérification formelle, Systèmes à compteurs, Programmes avec pointeurs, Logique temporelle, Model-checking
Page personnelle d'Arnaud Sangnier.