Proposition de stage de recherche Master M1/M2

Titre

: Vérification des communications FIFO

Encadrants

: Alain Finkel (LSV), Étienne Lozes (LSV / Aix-La-Chapelle)

Lieu

: LSV, Aix-La-Chapelle.

Contact

: {finkel,lozes}@lsv.ens-cachan.fr

1  Contexte

Un automate à files FIFO est un automate assez similaire syntaxiquement à un automate à piles, ne comportant que deux types de transition, enfilage et defilage d’une lettre, mais il manipule des files et non des piles. Ces automates à files permettent de modéliser le coeur de nombreux protocoles, (voir par exemple l’outil Heap-Hop[5]). Malheureusement, c’est un exemple de système infini pour lequel la plupart des questions liées à la sûreté de ces protocoles sont indécidables en général (par exemple, contrairement aux piles, une file suffit pour l’indécidabilité de la plupart des questions). Ceci a conduit à poser des restrictions sévères, rarement compatibles avec bon nombre de protocoles réalistes, pour en faire un modèle décidable.

Si l’on exclut ces restrictions, les travaux sur ce modèle ont essentiellement porté sur diverses techniques de calcul de point fixe (notamment l’accélération de boucle[1, 2], le widening[3], ou l’approche CEGAR[4]). Toutefois, ces travaux ne peuvent pas vérifier certains protocoles car le domaine abstrait, la représentation symbolique d’ensembles infinis de configurations, n’est pas assez expressif - en général, elle se ramène à un codage en langage régulier.

2  Objectif du stage

L’objectif de ce stage est d’étudier une classe de domaines abstraits plus riche que les langages réguliers, les Parikh Finite Automata (PFA) - intuitivement, des automates finis dans lesquels on impose des contraintes arithmétiques sur le nombre de fois où chaque transition est utilisée dans un mot accepté. Les résultats existants d’accélération d’une boucle à partir d’un PFA, ont un coût algorithmique important ce qui explique qu’aucun de ces résulats n’ait incité à les implémenter. Nous proposons de dégager la bonne notion de PFA qui serait à la fois robuste pour les calculs de point fixe et efficace d’un point de vue algorithmique. Suivant la vitesse d’avancemenent, il serait aussi envisageable d’implémenter ce domaine abstrait et de le tester sur des exemples de protocoles.

Références

[1]

Bernard Boigelot and Patrice Godefroid. Symbolic verification of communication protocols with infinite state spaces using qdds (extended abstract). In Rajeev Alur and Thomas A. Henzinger, editors, CAV, volume 1102 of Lecture Notes in Computer Science, pages 1–12. Springer, 1996.

[2]

Ahmed Bouajjani and Peter Habermehl. Symbolic reachability analysis of fifo channel systems with nonregular sets of configurations (extended abstract). In Pierpaolo Degano, Roberto Gorrieri, and Alberto Marchetti-Spaccamela, editors, ICALP, volume 1256 of Lecture Notes in Computer Science, pages 560–570. Springer, 1997.

[3]

Tristan Le Gall, Bertrand Jeannet, and Thierry Jéron. Verification of communication protocols using abstract interpretation of fifo queues. In Michael Johnson and Varmo Vene, editors, AMAST, volume 4019 of Lecture Notes in Computer Science, pages 204–219. Springer, 2006.

[4]

Alexander Heußner, Tristan Le Gall, and Grégoire Sutre. Extrapolation-based path invariants for abstraction refinement of fifo systems. In Corina S. Pasareanu, editor, SPIN, volume 5578 of Lecture Notes in Computer Science, pages 107–124. Springer, 2009.

[5]

Jules Villard, Étienne Lozes, and Cristiano Calcagno. Tracking heaps that hop with heap-hop. In Javier Esparza and Rupak Majumdar, editors, Proceedings of the 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’10), volume 6015 of Lecture Notes in Computer Science, pages 275–279, Paphos, Cyprus, March 2010. Springer.

Ce document a été traduit de L^AT_EX par H^EV^EA