Réduction d'ordre partiel pour les systèmes temporisés

Abstract

Dans cette thèse, nous étudions le problème d'accessibilité dans les réseaux d'automates temporisés. Nous nous concentrons sur la question de l'explosion de l'espace d'états causée par les entrelacements d'actions dans les exécutions de ces réseaux. Nous proposons deux solutions différentes pour atténuer l'effet de cette explosion combinatoire. La première est un algorithme d'accessibilité basé sur une sémantique temporelle locale pour les réseaux d'automates temporisés. La seconde est un cadre pour les méthodes de réduction d'ordre partiel pour ces mêmes réseaux.L'approche standard pour résoudre le problème d'accessibilité d'un automate temporisé implique l'exploration d'un graphe dirigé, connu sous le nom de graphe de zone de cet automate.Dans notre travail, nous considérons une sémantique alternative pour les réseaux d'automates temporisés, appelée sémantique temporelle locale, qui a été introduite par Bengtsson et al [BJLY98], ainsi que la notion correspondante de graphes de zone locale. Cette nouvelle approche consiste à considérer une échelle de temps locale à chaque processus, et à ne synchroniser ces temps locaux que lorsque les processus exécutent une action commune. Le principal défi ici est que les graphes de zones locales sont infinis en général. Nous surmontons ce défi en concevant un nouvel algorithme qui vérifie l'accessibilité dans un réseau en calculant une troncature finie de son graphe de zone locale. Nous montrons que plusieurs nœuds dans le graphe de zone standard, qui correspondent à différents entrelacements des mêmes actions, sont remplacés par un seul nœud dans le graphe de zone locale. L'évaluation expérimentale de notre algorithme montre le gain d'un ordre de grandeur par rapport aux algorithmes de référence sur plusieurs exemples standards.Dans la deuxième partie de cette thèse, nous nous concentrons sur l'application des techniques de réduction d'ordre partiel à l'exploration des graphes de zones locales. La réduction d'ordre partiel est une technique largement utilisée pour combattre l'explosion combinatoire de l'espace d'états. Elle consiste à identifier une petite partie de l'espace d'états dont l'exploration est suffisante pour vérifier le système. Nous décrivons pourquoi ceci est difficile à réaliser dans un cadre temporisé. Nous identifions ensuite une sous-classe de réseaux d'automates temporisés, que nous appelons systèmes à désynchronisation bornée, pour lesquels nous développons des algorithmes de réduction d'ordre partiel. Nous présentons plusieurs exemples pour cette sous-classe, motivés par des benchmarks standards. Nous fournissons également une évaluation d'un prototype de l'implémentation de ces méthodes en utilisant l'outil TChecker.