sujet-these-cpt pile horl

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 ...