Valérie Murat

Les systèmes informatiques sont de plus utilisés, et on doit donc s'assurer de leur fiabilité. La vérification formelle d'un système permet d'établir un diagnostic précis pour une propriété donnée, et de retourner un contre-exemple si la propriété n'est pas vérifiée.
Pour vérifier certains systèmes intéressants comme les protocoles de sécurité, les réseaux ou les programmes Java, on doit considérer un espace d'états infini. L'ARTMC (Abstract Tree Regular Model Checking) permet de vérifier des propriétés de sûreté sur des systèmes à espaces d'états infinis en utilisant des automates d'arbres et des transducteurs d'arbres, ou des systèmes de réécriture.

Les propriétés de sûreté permettent de vérifier qu'il n'y a pas d'état accessible par le système qui ne satisfait pas la propriété, i.e. pas d'état erreur. Pour vérifier une propriété de sûreté, il faut calculer l'ensemble de tous les états accessibles par le système, et vérifier qu'il n'y a aucun état erreur dans cet ensemble, grâce à une opération d'intersection. On appelle cette vérification une analyse d'atteignabilité.
Quand les états sont représentés par des termes, l'ensemble des états accessibles est calculé grâce à un transducteur d'arbres ou grâce à un système de réécriture. Un système de réécriture est un semble de règles de réécriture l → r permettant de réécrire un ensemble de termes.
Par exemple, f(x,y) → f(g(x),g(y)) est une règle de réécriture, et le terme f(a,b) est réécrit de cette manière : f(a,b) → f(g(a),g(b)) → f(g(g(a)),g(g(b))) → f(g(g(g(a))),g(g(g(b)))) → ...

Dans l'ARTMC (Abstract Tree Regular Model Checking), une configuration (ou état) du système est représentée par un terme, i.e. un mot construit avec des symboles fonctionnels qui peut être représenté par un arbre (ex: f(g(a),b) ).
Un ensemble (possiblement infini) de termes est représenté par un automate d'arbres, composé d'un ensemble d'états, un ensemble d'états finaux, un alphabet de symboles fonctionnels, et un ensemble de transitions normalisées. Par exemple, l'ensemble de transitions d'un automate d'arbres {a → q₁, b → q₂, g(q₁) → q₃, f(q₃,q₂) → q_f } peut reconnaître le terme f(g(a),b).

TimbukLTA est une extension de Timbuk, i.e. un outil de complétion d'automates d'arbres pour l'analyse d'atteignabilité des systèmes de réécritures, cette extension utilisant les automates d'arbres à treillis (Lattice Tree Automata) pour représenter (efficacement) des domaines infinis tels que les entiers, les chaines de caractères, etc., et améliore grandement l'efficacité de la vérification des programmes Java (voir Publications → Rapports techniques).
Code source et informations.
© 2012 ‒ Thomas Genet, Valérie Murat et Tristan Le Gall

CopsterLTA est une extension de Copster. Depuis un fichier .class obtenu en compilant des fichiers .java, Copster produit un système de réécriture simulant l'exécution du programme Java. CopsterLTA utilise l'arithmétique sur les entiers et symboles interprétables plutôt que l'arithmétique de Peano comme c'était le cas dans Copster. CopsterLTA intègre également des règles de réécriture conditionnelles. Le système de réécriture généré par CopsterLTA peut ensuite être vérifié en utilisant TimbukLTA.
Code source et informations.
© 2012 ‒ Valérie Murat, Nicolas Barré, Laurent Hubert, Luka Le Roux et Thomas Genet