L'analyse d'accessibilité est généralement l'approche utilisée pour la validation des protocoles. Le problème posé par l'application de cette technique est celui de l'explosion combinatoire. Dans cet article, nous proposons une nouvelle technique de validation de protocoles appelée Reverse Leaping Reachability Analysis (RLRA). Au lieu de parcourir tout l'espace des états de protocole, notre approche explore seulement un ensemble réduit de cet espace afin de détecter les erreurs de type Interblocage. Les résultats d'expérimentation ont montré que notre technique permet de réduire la taille du graphe d'accessibilité de protocole est donc réduire le problème de l'explosion combinatoire. Mots-clé: validation de protocoles, automate à états complexes, interblocage
Dans le domaine des Services Web, les protocoles de communication peuvent être modélisés sous forme de communication d'automates à états finis. Dans ce modèle, le comportement de chaque entité communicante est spécifié par un Automate à Etats Finis (AEF). Ces entités échangent des messages via des canaux de communication de capacité limitée. La validation de protocoles, consiste à vérifier l'absence des erreurs logiques de spécification telles que les erreurs d'interblocage et les réceptions non spécifiées. L'analyse d'accessibilité standard est généralement l'approche la plus utilisée dans le domaine de validation de protocoles. Le principe de cette technique est l'énumération de toutes les interactions possibles entre les entités communicantes. Cette énumération génère des états globaux de protocole où chaque état global donne la situation du protocole après avoir exécuté une opération. A la fin de cette opération, on obtient un graphe d'accessibilité de protocole. Les erreurs de protocole, sont alors détectées par la vérification de chaque état global composant ce graphe. L'analyse d'accessibilité standard est une technique intuitive, simple et permet la détection de toutes les erreurs que peut contenir une spécification de protocole. Cependant, elle soufre du problème de l'explosion combinatoire. En général, le nombre total des états globaux d'un protocole est exponentiel en terme de nombre d'entité composant le protocole ainsi que le nombre d'état local de chaque entité [4]. Bien que plusieurs versions (améliorations) ont étés proposées [1,2,3] pour allégir l'analyse d'accessibilité standard, le problème de l'explosion combinatoire était toujours présent, ce qui a limité leur application à des protocoles simples.
L'analyse d'accessibilité réversible [5] est une alternative intéressante de l'analyse d'accessibilité standard. A partir des propriétés qui caractérisent les erreurs de type interblocage, on dégage un ensemble d'états globaux qui vérifient ces propriétés. Ces états sont appelés états suspects. Par la suite, un état suspect est confirmé comme une erreur d'interblocage si l'état global initial du protocole est atteignable par une opération de retour arrière à partir de cet état suspect, sinon l'état suspect est retiré de l'ensemble des erreurs de protocole. Avec ce procédé, cette technique permet de parcourir seulement un sous-ensemble de l'espace des états du protocole. Bien que cette technique permet de réduire l'espace des états à explorer durant l'analyse, le problème de l'explosion combinatoire peut se présenter pour une validation de protocole complexe. Donc, pour rendre cette approche de validtion efficace nous avons besoin d'optimiser la construction des chemins de retour arrière.
Dans cet article, nous proposons une technique de validation de protocoles modélisés sous forme de Communication d'Automate d'Etats Finis Complexes (CAEFC), appelée RLRA (Reverse Leaping Reachability Analysis). Notre technique, permet la détection de toutes les erreurs de type interblocage dans une spécification de protocole. En se basant sur une approche de validation avec retour arrière, on commence par identifier de possibles états d'interblocage ensuite, valider parmi ces états suspects, ceux qui présentent réellement une erreur à travers la recherche de chemins de retour vers la racine du graphe de protocole. Pour réduire le problème de l'explosion combinatoire, nous introduisons les graphes de sauts (leap graphe) que nous exploitons dans la construction des chemins de retour arrière. Ces graphes de sauts, permettent d'éviter le parcourt des états globaux qui ne sont pas utiles dans l'analyse, ce qui apporte une réduction importante sur la taille du graphe à parcourir. Pour chaque erreur confirmée, nous donnons aussi sa nature (simple, hybride ou complexe) selon la nature des états qui présentent l'erreur.
Le reste de cet article est organisé comme suite : La prochaine section introduit le modèle de CAEFC. La section trois, explique notre approche de validation ainsi que les prouves formelles de son applicabilité. La quatrième section, donne les résultats d'expérimentation. La dernière section est une conclusion de ce travail.
Complexes (CAEFC) [9] Un modèle de CAEFC introduit la notion d'état complexe, qui est un AEF dont certains de ses états sont eux-mêmes des AEF (internes
On definie la fonction act() comme suite [8] :
1. Pour une transition t ∈ ∆ i , act(t) = i est l'indice de l'entité auquel appartient la transition t, 2. Pour un ensemble de transition T , act(T ) = {i ∈ I/T ∩∆ i = ε} est l'ensemble des indices des entités qui ont au moins une transition dans T ;
Nous définissons également la fonction F ront(c G ij ) qui renvoie le message en tête du canal c ij à l'état global G.
En plus de la nature de l'erreur logique, l'utilisation des automates d'états complexes nécessite la définition du type de l'erreur détectée qui peut être de type simple, lorsque chaque entité communicante se trouve dans un de ses états simples, complexe lorsque toutes les entités se trouvent dans un de leurs états complexes et hybride lorsque une ou plusieurs entités du modèle se trouvent dans un état simple et le reste des entités se trouvent dans des états complexes.
La validation d'un protocole revient à faire une analyse de son graphe d'accessibilité. Un graphe d'accessibilité donne les différentes exécutions possibles du protocole, les noeuds de ce graphe sont les états globaux du protocole et les arcs sont les différentes transitions (interactions) qui font passé le protocole d'un état global vers un autre. L'approche de validation exhaustive soufre du problème de l'explosion combinatoire qui est dû au grand nombre d'état global à générer pendant l'analyse. Ce problème peut être réduit en adoptant une approche de validation avec retour arrière. Cette approche est appelée analyse d'accessibilité réversible (RRA ) [5]. Dans cette approche, on génère l'espace des états de protocole d'une manière réversible. A partir d'un ensemble d'états, dit indésirable, on essaye d'accéder l'état global initial par une opération de retour arrière. L'ensemble des états indésirables est composé des états globaux qui présentent des caractéristiques d'un état d'interblocage (chaque entité est dans un état d'attente de réception d'un message et l'état de leurs canaux d'entrée est vide).
Dans cette section, nous proposons une technique de validation de protocoles qui est basée sur une approche avec retour arrière. Dans notre approche de retoure arrière, au lieu de travailler sur un graphe d'accessibilité standard (couvre tout l'espace des états), nous utilisons un graphe de sauts (LRA3 ) [8]. Ce graphe est construit à partir d'un sous ensemble de l'espace des états de protocole. La particularité de ce graphe c'est qu'il couvre aussi tous les états qui peuvent présenter une erreur de type interblocage. Donc, l'utilisation d'un graphe de sauts réduit le nombre d'état à parcourir tout en gardant la capacité de détecter toutes les erreurs d'interblocage, ce qui permet de réduire la complexité du l'analyse de protocole.
Un graphe de sauts est un graphe d'accessibilité réduit. Cette réduction est obtenue du fait que le passage d'un état global vers un autre peut se faire via l'exécution de plusieurs transitions à la fois, ce qui permet d'éviter de générer des états intermédiaires résultants de l'exécution de chaque transition à part. les transitions qui peuvent s'exécuter en même temps sont appelées : transitions simultanément exécutables.Ces transitions simultanées forme un saut dans un graphe d'accessibilité. L'ensemble des transitions d'envoi ou de réception de messages de l'entité P i , qui sont exécutables à l'état globale G, sont notés respectivement
. L'ensemble de toutes les transitions des différentes entité communicantes du protocole qui sont exécutables à l'état G, est noté :
Transitions potentiellement exécutables : Une transition de réception de message t = (s i , +y, s i ) est dite potentiellement exécutable à l'état global G, ssi
la capacité des canaux de communication du système. L'ensemble des transitions de réception de message et des transitions d'envoi de message de l'entité P i qui sont potentiellement exécutables à l'état globale G, sont noté respectivement P + i (G) et P − i (G). L'ensemble de toutes les transitions potentiellement exécutables de l'entité P i est noté :
Lors de la construction d'un graphe de sauts, les transitions à exécuter simultanément, doivent être exécutables dans le même état global et doivent appartenir à des entités du protocole qui ne disposent pas de transitions potentiellement exécutables [8]. Un ensemble de telles transitions est appelé saut, noté pleap (proper leap). Donc, un saut est un ensemble non vide de transitions : T ⊆ X(G), tel que pour toute transition t, t ∈ T , act(t) = act(t ) si t = t (i.e T contient au plus une transition exécutable de chaque entité). Les différents ensembles de T , construits à l'état global G, forment un ensemble de sauts noté pleap(G).
Definition 1 (Calcul de l'ensemble pleap (sauts) [7]). Soit G un état global. On note par W ait(G), l'ensemble des indices des entités qui disposent d'une transition potentiellement exécutable à l'état G. Cet ensemble est définit par : W ait(G) = {i ∈ I/X i (G) =⇒ P i (G) = }. L'ensemble des sauts pleap(G) est donc calculé comme suite :
Avant de calculer l'ensemble pleap(G) , on doit calculer l'ensemble W ait(G) pour identifier les entités qui disposent de transitions potentiellement exécutables. Si toutes les entités appartiennent à l'ensemble W ait(G) ça veut dire qu'il n'y a pas de saut à faire à partir de G et dans ce cas la, on exécute chaque transition de X(G) indépendamment des autres (transitions simples). Si W ait(G) est inclut dans I, l'ensemble de sauts à exécuter à partir de G (pleap(G)) sera le produit cartésien des ensembles de transitions exécutables de chaque entité Xi(G) i.e pleap(G)
Definition 2 (transition de saut [8]). Une transition de saut est une relation binaire sur un ensemble d'états globaux, elle est notée :
), G1→ l G2 existe, ssi il existe un ensemble de transitions T appartenant à l'ensemble de sauts pleap(G1), tel que l'exécution simultanée des transitions de T , fait passer le protocole à l'état global G2. Soit → l * la fermeture transitive et réflexive de → l . G2 est dit accessible par sauts depuis G1, ssi G1 → l * G2. Si G1 = S0 (état global initial du protocole), G2 est dit être accessible par saut. On dénote par L Π l'ensemble de tous les états du protocole qui sont accessibles par sauts. Pour une séquence d'ensemble de sauts Ω = T 1, T 2, T 3 . . . , T m, G1 → l * G2 dénote l'existence des états globaux Q0, Q1, Q2 . . . , Qm , tel que :
Dans un graphe de sauts, les neouds sont des états globaux qui sont accessibles par des sauts. Le calcul des transitions de sauts (pleap) se fait au niveau de chaque état global, en commençant de l'état global initial du système.
Dans ce qui suit, nous donnons les définitions qui vont nous permettre de construire un graphe de sauts d'une manière réversible. L'opération de retour arrière peut être vue comme une procédure abstraite. A partir d'un état global on monte vers la racine, et dans ce cas-là, les transitions d'envoi de messages vont être traitées comme étant des transitions de réception de messages, et les transitions de réception de messages vont être traitées comme étant des transitions d'envoi de messages.
Transitions simultanément et réversiblement exécutables. Comme pour la construction des graphes de sauts, nous avons besoin de définir les notions de transitions réversiblement exécutables et de transitions potentiellement et réversiblement exécutables afin de calculer les transitions simultanément et réversiblement exécutables (sauts réversibles).
. L'ensemble de toutes les transitions du protocole, qui sont réversiblement exécutables à l'état G, est noté :
Transition potentiellement et réversiblement exécutable : Une transition de réception de message t = (s i , +y, s i ), avec y ∈ M i , est dite potentiellement et réversiblement exécutable à l'état global réversible G, ssi
Les ensembles des transitions de réception de messages et des transitions d'envoi de messages de l'entité P i , qui sont potentiellement et réversiblement exécutables à l'état global G, sont notés
Comme pour la construction d'un graphe de sauts, la construction d'un graphe de sauts réversibles se fait par le calcul des transitions simultanément et réversiblement exécutables, ces transitions doivent être exécutables dans le même état global réversible et doivent appartenir à des entités du protocole qui ne disposent pas de transitions potentiellement et réversiblement exécutables. Un ensemble de telles transitions est appelé sauts réversibles, noté pleap R (reverse proper leap). Donc, un saut réversible est un ensemble non vide de transitions : T ⊆ X R (G), tel que pour toute transition t, t ∈ T , act(t) = act(t ) si t = t (i.e T contient au plus une transition réversiblement exécutable de chaque entité). Les différents ensembles T , construits à l'état global réversible G, forment un ensemble de sauts réversibles noté pleap R (G).
Nous donnons dans ce qui suit la définition formelle de l'ensemble des sauts réversibles pleap R . Definition 4 (calcul de l'ensemble pleap R ). Soit G un état global réversible. On définit l'ensemble des entités qui disposent d'une transition potentiellement et réversiblement exécutable à l'état G par :
Avant de calculer l'ensemble pleap R (G), on doit calculer l'ensemble W ait R (G) pour identifier les entités qui disposent de transitions potentiellement et réversiblement exécutables. Si toutes les entités appartiennent à l'ensemble W ait R (G) ça veut dire qu'il n'y a pas de saut réversible à exécuter à partir de G, et dans ce cas la, on exécute chaque transition de X R (G) indépendamment des autres (simple transition). Si l'ensemble W ait R (G) est inclut dans I, l'ensemble de sauts réversibles pleap R (G) sera le produit cartésien des ensembles de transitions réversiblement exécutables de chaque entité
Definition 5 (transition de saut réversible). Une transition de saut réversible, est une relation binaire → R sur un ensemble d'états globaux réversibles. Pour deux états globaux réversibles G1 = (< s
existe, ssi il existe un ensemble de transitions réversiblement exécutables T ∈ pleap R (G1), tel que l'exécution des transitions de T à partir de G1 donne l'état global G2. La relation de transition G1 → R G2 signifie que l'état global G2 est obtenu d'une manière réversible directe depuis l'état global G1. Soit → R * la fermeture transitive et réflexive de → R , on dit que l'état G2 est accessible par saut réversible de puis G1, ssi G1 → R * G2. Le chemin qui relie G1 vers G2 est alors appelé : chemin de sauts réversibles de G1 vers G2.
Dans cette section, nous expliquons l'utilisation des sauts réversibles pour la détection des erreurs d'interblocage. Definition 6 (état suspect d'interblocage [5]).
est un état de réception de message pour tout i ∈ I.
Definition 7 (état d'interblocage [8]). Un état global G = (< s G i > i∈I , < c G ij > (i,j)∈L ) est dit état d'interblocage ssi :
1. ∀(i, j) ∈ L : c G ij = ε et s G i est un état de réception de message pour tout i ∈ I ; 2. L'état global G est accessible par sauts à partir de G0.
Un état global est dit état d'interblocage lorsque tous les canaux de communications dans cet état sont vides et toutes les entités du protocole sont dans un état de réception de messages.
Nous donnons ci-dessous, le théorème principal de notre proposition, qui nous permettra d'utiliser les chemins de sauts réversibles afin de détecter les erreurs logiques de type interblocage.
Theorem 1. Soit P i = (P, L) un protocole et soit GS un état global suspect d'interblocage. L'état suspect d'inter blocage GS, est confirmé comme état d'inter blocage ssi, l'état global initial du protocole G0 est accessible par un chemin de sauts réversibles à partir de l'état suspect GS.
On se basant sur le théorème 1, la détection des états d'interblocage, peut être faite par une vérification de l'accessibilité par sauts réversibles de l'état initial du système en partant d'un état suspect.
Dans cette section, nous donnons l'algorithme de notre approche de validation. Pour des raisons de simplifications, nous traitons des protocoles de communication entre deux entités seulement. Notre algorithme peut être facilement généralisé sur une communication entre plusieurs entités.
Les états suspects d'interblocage sont obtenus par une combinaison, des états locaux de réception de messages, des différentes entités communicantes du protocole (Définition 6). Cette phase est implémentée par l'Algorithme 1 du calcul d'états suspects.
Le test de la ligne 4 de l'algorithme sert à écarter les états locaux qui sont finaux car un état global final ne peur être état d'interblocage.
Afin de confirmer l'existence d'une erreur dans un état suspect GS, l'algorithme effectue une recherche d'un chemin de sauts réversibles vers l'état initial du protocole. Cette phase est donnée sur l'Algorithme 2. L'ensemble Explored est utilisé pour marquer les états globaux qui sont déjà traités (vérifiés). Chaque nouvel état global n'appartenant pas à Explored, sera mis dans Open afin de le traiter dans la prochaine itération (ligne 20-21-22). A partir de chaque état global G (non traité), nous calculons tous les ensembles des transitions simultanément exécutable (T ) de cet état global, par l'utilisation de la définition 4 (ligne 18).
Pour chaque T obtenu et qui est un saut réversible, nous générons un nouvel état global. L'algorithme continue son exécution jusqu'à ce que soit l'état initial est atteint, et dans ce cas la l'erreur logique est confirmée dans l'état suspect GS, soit il ne reste plus d'état à explorer et donc l'erreur logique est écartée. Les lignes de code de 7 à 16 permettent d'identifier le type de l'erreur détectée (simple, hybride ou complexe), selon la nature des états locaux composant l'état de l'erreur.
Pour montrer l'efficacité de notre technique, nous avons choisi de la comparer avec une technique de la même famille, c'est-à-dire une technique qui utilise le principe de
Dans cet article, nous avons proposé une technique de validation de protocoles basée sur une approche de validation avec retour arrière. Pour rendre l'analyse plus efficace, nous avons optimisé l'opération de construction des chemins de retour arrière. Cette optimisation est obtenue par l'utilisation de la technique de construction des graphes de sauts(LRA). L'utilisation de LRA nous a permet d'éviter de parcourir des états qui ne sont pas utiles dans l'analyse, ce qui nous a permet de réduire considérablement la taille du graphe d'accessibilité.