sujet-these-cpt pile horl

Description

1Proposition d’un sujet de stage de M2 et/ou de thèseLieu : Laboratoire Spécification et VérificationÉcole Normale Supérieure de Cachan61, avenue du Président Wilson94235 Cachan CEDEXTitre : Vérification de systèmes à compteurs avec piles et horlogesDescription du sujet : La vérification de systèmes informatiques manipulant des comp-teurs, des piles et des horloges est un problème difficile [BFLP03,L03,B05] ne serait-ceque parce de nombreux problèmes de vérification comme par exemple le problème del’atteignabilité sont indécidables pour les automates à compteurs. D’un autre côté, ilexiste quelques outils performants qui arrivent à calculer les ensembles d’états (ou debonnes approximations) des automates à compteurs que l’on rencontre dans les étudesde cas industrielles. En particulier, l’outil FAST développé au LSV, a permis de vérifieravec succès plusieurs études de cas difficiles dont un protocole de communication pourles systèmes embarqués (le TTP). Pour traîter ces études de cas, il est pratique de dis-poser du modèle des systèmes à compteurs qui est plus expressif que celui des automatesà compteurs.Une transition entre états de contrôle d’un système à compteurs est une fonction affinequidonnelesnouvellesvaleursdescompteurslorsqueceux-ciprennentleursvaleursdansl’ensemble de définition qui doit être définissable dans l’arithmétique de Presburger.FASTprendenentréeunsystèmeàcompteursetunensembled’étatsinitiauxégalementdonné par une formule de Presburger et ...

Informations

• Publié par: Hibos
• Nombre de lectures: 31
• Langue: Français

Extrait

1 Proposition d’un sujet de stage de M2 et/ou de thÈse

Lieu :Laboratoire Spcification et Vrification Ècole Normale Suprieure de Cachan 61, avenue du Prsident Wilson 94235 Cachan CEDEX Titre :VÉrification de systÈmes À compteurs avec piles et horloges Description du sujet :La vrification de systmes informatiques manipulant des comp- teurs, des piles et des horloges est un problme difficile [BFLP03,L03,B05] ne serait-ce que parce de nombreux problmes de vrification comme par exemple le problme de l’atteignabilit sont indcidables pour les automates À compteurs. D’un autre cÔt, il existe quelques outils performants qui arrivent À calculer les ensembles d’tats (ou de bonnes approximations) des automates À compteurs que l’on rencontre dans les tudes de cas industrielles. En particulier, l’outil FAST dvelopp au LSV, a permis de vrifier avec succs plusieurs tudes de cas difficiles dont un protocole de communication pour les systmes embarqus (le TTP). Pour trater ces tudes de cas, il est pratique de dis- poser du modle des systmes À compteurs qui est plus expressif que celui des automates À compteurs. Une transition entre tats de contrÔle d’un systme À compteurs est une fonction affine qui donne les nouvelles valeurs des compteurs lorsque ceux-ci prennent leurs valeurs dans l’ensemble de dfinition qui doit tre dfinissable dans l’arithmtique de Presburger. FAST prend en entre un systme À compteurs et un ensemble d’tats initiaux galement donn par une formule de Presburger et calcule les formules reprsentant l’acclration des circuits du graphe de contrÔle du systme À compteurs. Qand le systme est ap- platissable, c’est-À-dire quand son ensemble d’tats accessibles est gal À celui d’un de ses sous-systmes sans circuits imbriqus, FAST calcule une formule de Presburger qui reprsente l’ensemble des tats accessibles. La complexit au pire de FAST est leve puisque sa brique de base d’acclration d’un circuit est 3-exptime. Cela n’empche pas d’observer que dans la pratique cette complexit au pire n’est pas atteinte. Les automates temporiss de Alur et Dill [AD94] ont de meilleures proprits algorith- miques gráce À une reprsentation symbolique des ensembles de configurations efficace et facilement manipulable. Ces ensembles de configurations sont expressibles dans un fragment de l’arithmtique de Presburger dont la complexit est polynomiale. De mme, les automates À pile ont un ensemble rationnel d’tats accessibles qui est calculable en temps polynomial. Considrer des automates temporiss discrets, voir par exemple [DJ99,DSPK03], est une faÇon de manipuler À la fois des horloges et des compteurs. Cependant, trs peu d’outils de vrification peuvent traiter de tels systmes, voir par exemple [ABS01]. Il existe de nombreuses recherhces sur les systmes temporiss et hybrides mais finalement peu de recherches ont t menes visant À analyser ces modles htrognes (contenant À la fois des variables entires, des mots et des variables relles) en combinant les reprsentations symboliques efficaces pour chacun des types de donnes. Des recherches rcentes examinent galement les diffrents manires d’introduire la tem- porisation dans les rseaux de Petri et comparent la puissance d’expression de ces mo- dles.

2

Le but de la thse est d’tudier les modles existants qui manipulent À la fois des comp- teurs, des piles et des horloges et d’en dgager des classes intressantes pour lesquelles de nombreux problmes de vrification soient algorithmiquement traitables (accessibilit, vivacit, etc.). L’objectif est de pouvoir vrifier les proprits des systmes À compteurs, À piles et À horloges afin de pouvoir vrifier des abstractions plus ralistes de systmes rels. Bibliographie : [ABS01] A. Annichini, A. Bouajjani, M. Sighireanu. TReX : a tool for reachability ana- lysis of complex systems. In Proc. of CAV’01, Paris, pages 368-372, 2001. [AD94] R. Alur, D. Dill. A theory of timed automata. Theoretical Computer Science 126 : 183-235, 94. [B05] S. Bardin. Vers un model-checking avec acclration plate de systmes htrognes. Thse de doctorat de l’ENS de Cachan, 2005. [BF04] S. Bardin and A. Finkel. Composition of accelerations to verify infinite hete- rogeneous systems. In Proceedings of the 2nd International Symposium on Automated Technology for Verification and Analysis (ATVA’04), Taipei, Taiwan, ROC, October- November 2004, LNCS 3299, pages 248-262. Springer. [BFLP03] S. Bardin, A. Finkel, J. Leroux, L. Petrucci. FAST : Fast Acceleration of Symbolic Transition Systems. In Proc. of CAV’03, Boulder, pages 118–121, 2003. [CJ99] H. Comon, Y. Jurski. Timed automata and the theory of real numbers. In Proc. of CONCUR’99, Eindhoven, pages 242-257, 1999. [DSPK03] Z. Dang, P. San Pietro, R. Kemmerer. Presburger Liveness Verification of Discrete Timed Automata. Theoretical Computer Science 299 :(1-3) : 413-438, 2003. [L03] J. Leroux. Algorithmique de la vrification des systmes À compteurs. Thse de doctorat de l’ENS de Cachan, 2003. Personne encadrant le stage : A. Finkel Tl : 01 47 40 75 69 Email :[e-mail]