Vérification d'automates temporisés : sûreté, vivacité et modélisation

Abstract

Cette thèse revisite les algorithmes standards pour les problèmes d'accessibilité et de vivacité des automates temporisés. L'algorithme standard pour tester l'accessibilité consiste à utiliser l'inclusion de zones pour explorer efficacement un arbre de recherche abstrait. Cependant, l'ordre du parcours du graphe a une forte incidence sur l'efficacité de l'algorithme. Dans cette thèse nous introduisons deux stratégies, nommées ranking et waiting, et une combinaison des deux. De nombreux exemples montrent que la combinaison des deux stratégies aide l'algorithme d'accessibilité à éviter des explorations non nécessaires. Le problème de vivacité est couramment vérifiées par l'analyse des cycles dans l'automate temporisé. Contrairement à l'algorithme d'accessibilité, l'algorithme pour l'analyse de vivacité ne peut pas librement utiliser l'inclusion de zones. Par conséquent, il y a des situations où l'algorithme doit faire une longue exploration avant de conclure l'existence d'un cycle. Nous proposons une analyse accélérée des cycles, nommées w-iterability checking, qui permet d'améliorer la performance de l'algorithme de vivacité des automates temporisés. En plus, nous proposons une modélisation du mécanisme de démarrage du protocole FlexRay. La modélisation permet à vérifier le mécanisme dans configurations différents du réseau FlexRay. Nous présentons également un outil de visualisation qui aide à mieux comprendre le fonctionnement des algorithmes d'analyse.