Développement prouvé d'un algorithme de vérification
théorie des automates finis, assistant de preuve, programmation fonctionnelle
| LSV | LORIA | |
| Laboratoire Spécification et Vérification | Laboratoire lorrain de recherche | |
| Ecole Normale Supérieure de Cachan | en informatique et ses applications | |
| 61 avenue du Président Wilson | Campus Scientifique, B.P. 239 | |
| 94235 Cachan cédex | 54506 Vandoeuvre-lès-Nancy cédex |
La théorie des automates finis joue un rôle éminent en informatique. Il existe en particulier une relation très forte entre les automates finis (opérant sur des objets finis ou infinis) et certaines théories logiques et arithmétiques. Cette relation est à la base d'une approche de la vérification algorithmique des systèmes appelée model-checking[1].
Dans cette approche, le système T et la propriété attendue P sont représentés par des automates, et la vérification est ramenée à la résolution d'un problème d'inclusion du langage L(T) dans L(P) . Traditionnellement, ce problème est résolu par une réduction au problème du vide du langage L(T x Pc), où Pc désigne l'automate qui accepte le complément du langage de P et "x" le produit synchronisé d'automates. Plusieurs algorithmes efficaces ont été proposés dans la littérature pour décider ce problème; néanmoins, en pratique les automates sont de grande taille, et le problème de l'explosion combinatoire reste un frein important pour l'application systématique des techniques du model-checking.
La technique des antichaînes a été introduite récemment pour s'attaquer à l'explosion combinatoire que l'on rencontre dans les problèmes de la théorie des automates finis. Par exemple, d'excellents résultats ont été obtenus pour le problème d'universalité des automates finis (qui demande si un automate fini donné accepte tous les mots finis) qui a une complexité exponentielle [2]. Cette technique consiste à identifier et exploiter la structure des graphes qu'on manipule. Ainsi, pour le problème d'universalité on utilise la construction des sous-ensembles pour déterminiser les automates finis, et on peut se rendre compte que cette construction a des propriétés spécifiques exploitables algorithmiquement. En pratique, cette technique permet d'analyser des automates de 10.000 états contre une centaine d'états par les méthodes classiques.
Toujours dans le contexte de la vérification de systèmes, il est important de s'assurer de la correction de l'implémentation de l'algorithme de vérification afin de garantir la fiabilité du résultat. Ce problème devient non-trivial dès lors que les implémentations utilisent des structures de données compliquées ou mettent en oeuvre des optimisations avancées, et des erreurs compromettant la correction ont été trouvées dans plusieurs outils de model-checking.
Au cours de ce stage on s'intéressera à l'utilisation d'un assistant à la preuve comme Isabelle [3] pour générer une implémentation exécutable et digne de confiance pour l'algorithme basé sur les antichaînes qui résout le problème d'universalité pour les automates finis. Dans un premier temps on formalisera les constructions élémentaires nécessaires sur les automates finis dans la logique de l'assistant à la preuve. Ensuite on décrira l'algorithme à travers des définitions qui ressemblent à un programme fonctionnel, et on démontrera la correction de cet algorithme. Isabelle dispose d'un mécanisme de génération de code à partir de telles définitions, et on évaluera l'efficacité du code généré. L'objectif est d'obtenir une implémentation prouvée dont l'efficacité est proche de celle d'une implémentation conventionnelle existante. Des travaux récents [4, 5] nous laissent penser que cet objectif peut être atteint.
Le sujet demande des solides connaissances de base en théorie d'automates, ainsi qu'un goût pour les techniques formelles de modélisation et de vérification. Une expérience avec l'utilisation d'un assistant interactif à la preuve (comme Coq, HOL, Isabelle ou PVS) sera appréciée.
Les personnes encadrant ce stage sont:
| Laurent Doyen | Stephan Merz | |
| Tél.: 01 47 40 77 06 | Tél.: 03 54 95 84 78 | |
| doyen@lsv.ens-cachan.fr | Stephan.Merz@loria.fr | |
| http://www.lsv.ens-cachan.fr/~doyen/ | http://www.loria.fr/~merz/ |
Ce document a été traduit de LATEX par HEVEA