Algorithms for model-checking flat counter systems
Amit Kumar Dhar · 2014
Les systemes automatises font desormais partie integrante de notre vie quotidienne et une grande partie de nos activites dependent de leur bon fonctionnement. Ces systemes devenant de plus en plus sophistiques et complexes, demontrer leur bon fonctionnement s'avere etre une tâche ardue. Parmi les approches permettant de garantir la fiabilite de ces systemes, les methodes de verification formelles consistent en une meilleure alternative que la simulation ou le test qui doivent prendre en compte un nombre toujours plus important de possibles scenarios qui peuvent se produire lors de l'execution du systeme. La methode par model-checking est une des techniques developpes pour la verification formelle de systemes. Elle consiste a proposer des algorithmes permettant de verifier si un modele representant les executions possibles du systeme verifie une specification donnee sous la forme de formules logiques. Un des problemes du model-checking vient du fait que lorsque les modeles sont trop expressifs, les probleme de verification deviennent indecidables, il est alors impossible de proposer des algorithmes et ce meme pour des proprietes specifiant des comportement tres simple comme la non-accessibilite d'un etat d'erreur. Dans cette these, nous nous interessons au probleme du model-checking pour le modele des systemes a compteurs plats qui peu- vent etre vus comme des programmes manipulant un nombre fini de variables entieres (appelees aussi compteurs) et dont la structure de controle est restreinte. En ce qui concerne les logiques pour les specifications, nous prenons en compte les logiques temporelles traditionnelles (comme LTL, FO, CTL, etc) tout en les etendant afin d'exprimer egalement des proprietes sur la valeur prise par les compteurs lors des executions. Nous obtenons ainsi des specifications plus expressives. Nous fournissons, pour chaque classe de specifications, des algorithmes avec une complexite optimale permettant de resoudre le probleme du model-checking des systemes a compteurs plats. Notre ap- proche se base de plus sur une methodologie generale autorisant ainsi une possible reutilisation des resultats pour d'autres specifications.