Sujet : Accélération dans les domaines abstraits

Responsable : Jérôme Leroux et Grégoire Sutre
Téléphone : 05 40 00 35 09 et 05 40 00 33 36
e-mail : jerome.leroux@labri.fr et gregoire.sutre@labri.fr
Équipe : Méthodes Formelles
Thème : Modélisation et Vérification

Présentation du sujet :

La vérification d'un système se réduit souvent au calcul de l'ensemble des états atteignables. En général, cet ensemble est infini car le système manipule des variables évaluées dans un domaine infini (des variables entières, des horloges, des files de communication, etc). Pour décrire et manipuler ces ensembles infinis, on utilise des représentations symboliques. Par exemple, pour les systèmes à compteurs, on considère des contraintes linéaires [CH-POPL78] ou des automates arithmétiques [BW-ICALP02].

Les méthodes de vérifications basées sur des calculs symboliques se classent naturellement en deux familles: celles basées sur des calculs exacts et celles basées sur le raffinement d'abstractions. Ces deux familles de méthodes sont complémentaires. Les premières permettent de calculer, par une itération croissante, l'ensemble X des états atteignables. Les secondes sont guidées par la propriété à vérifier, et calculent, par une itération décroissante, une approximation supérieure suffisamment précise de X. Utilisées séparément, ces techniques ne permettent pas, en général, d'analyser des systèmes complexes de grande taille. Aussi, notre objectif consiste à réduire l'écart entre ces méthodes, en proposant notamment des techniques permettant de maîtriser l'imprécision lors des calculs approchés [GH-SAS06]. Nos premiers travaux [LS-SAS07, LS-FSTTCS07] dans ce sens cherchent à calculer de façon exacte le plus petit point fixe dans un treillis abstrait, ou en d'autres termes le plus petit invariant inductif représentable par un état abstrait. Le degré de précision est ainsi contrôlé par le choix du treillis abstrait (par exemple les intervalles, les octogones [M-PADO01], les octaèdres, etc), et le point fixe obtenu ne dépend pas de la manière dont il a été calculé.

L'objectif du stage est d'identifier des classes de systèmes et de treillis abstraits supportant des méthodes de calcul exact de plus petit point fixe. Dans un premier temps, on s'intéressera à la classe des réseaux de Petri et aux treillis des octogones [M-PADO01] et de ses extensions (octaèdres et ``templates´´)

Ce stage pourra être poursuivi par une thèse.

Mot-clés :

Vérification, système infini, représentation symbolique, accélération, interprétation abstraite.

Références :