Une technique de validation de protocoles basée sur une exploration avec retour arrière des automates complexes Farah Zoubeyr1 , Abdelkamel Tari1 , and Zahir Tari2 1 Département d’Informatique, Université Abderrahmane Mira de Béjaı̈a, Route de Targa Ouzemmour Béjaı̈a 06000, Algérie. zobifara@gmail.com, tarikamel@yahoo.fr 2 Royal Melbourne Institute of Technology (RMIT), Department of Computer Science, Melbourne, Australia. zahirtari@rmit.edu.au Résumé 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 ap- pelée Reverse Leaping Reachability Analysis (RLRA). Au lieu de parcou- rir 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 Inter- blocage. 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, inter- blocage 1 Introduction 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 Au- tomate à 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’in- terblocage 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 proto- coles. 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 2 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 plu- sieurs 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’ana- lyse 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 sus- pect, 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 com- binatoire 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 tech- nique, 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 en- suite, 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 proto- cole. 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 che- mins 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 intro- duit le modèle de CAEFC. La section trois, explique notre approche de valida- tion 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. 2 Modèle de Communication d’Automates à Etats Finis 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). Les états qui 3 rentrent dans la composition d’un état complexe sont appelés états internes. Le développement des différents AEF internes donne un AEF aplati, qui est un AEF ordinaire. Soit I = {1, 2, ..., n} un ensemble fini d’indices, avec cardinal(I)≥2. Dans un modèle de Communication d’automate d’états finis, un protocole Π est une paire (P, L), où P = {Pi /i ∈ I} est l’ensemble des n entités communicantes du protocole et L ⊆ I × I est la relation d’incidence non réflexive qui identifie un ensemble non vide de canaux de communication {Cij /(i, j) ∈ L}. Chaque canal Cij est une file FIFO, bornée et sans erreurs reliant l’entité Pi à l’entité Pj . Chaque entité Pi est un automate d’états finis : (Si ,S0i ,Efi ,Mi ,4i ) (simple ou complexe), composé d’un ensemble d’états Si , d’un ensemble d’états finaux Efi ,d’un alphabet de messages Mi ,d’un ensemble de transitions 4i et d’un état initial S0i . L’ensemble des états Si comprend des états simples et des états complexes. Chaque état complexe doit être défini par un AEF. Le contenu du canal Cij , noté cij , est une suite de messages de Mi , i.e. cij ∈ Mi∗ . Chaque canal peut contenir un nombre maximum de K (entier positif) messages. Une entité Pi envoie des messages sur son canal de sortie Cij (i, j ∈ I ∧ i 6= j) et reçoit des messages sur ses canaux d’entrées Cji (i, j ∈ I ∧ i 6= j). La relation de transition 0 4i est définie par :4i :Si × Mi → Si . Une transition t = (si , µ, si ) ∈ ∆i , définie à l’état local si de l’entité Pi , est dite transition d’envoi de message lorsque µ = −x, indiquant un envoi d’un message x (x ∈ Mi ) par l’entité Pi sur le canal Cij . t est dite transition de réception de message lorsque µ = +y, indiquant une réception d’un message y (y ∈ Mi ) par l’entité Pi depuis le canal Cji . Les signes - et + indiquent respectivement un envoi et une réception de message. Dans le 0 cas où si est un état complexe (représente un AEF interne), le résultat de la transition va mettre l’automate interne sur sont état initial, si si et aussi un état complexe, la transition ne peut être exécutée que si l’automate lui correspondant atteint sont état final. Un état global G du protocole Π est représenté par une paire (< sG i >i∈I G , < cGij > (i,j)∈L ), où sG i est l’état local de l’entité Pi et cij est le contenu du G0 canal Cij à l’état global G. L’état global initial est notée G0 = (< si >i∈I , < cG0 ij >(i,j)∈L ), tel que si G0 = S0i et cG0ij = ε , pour tout i ∈ I et (i, j) ∈ L. On definie la fonction act() comme suite [8] : 1. Pour une transition t ∈ ∆i , act(t) = i est l’indice de l’entité auquel appar- tient la transition t, 2. Pour un ensemble de transition T , act(T ) = {i ∈ I/T ∩∆i 6= ε} est l’ensemble des indices des entités qui ont au moins une transition dans T ; Nous définissons également la fonction F ront(cG ij ) qui renvoie le message en tête du canal cij à l’état global G. 4 2.1 Types d’erreur dans une spécification par modèle CAEFC 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. 2.2 Validation de protocoles La validation d’un protocole revient à faire une analyse de son graphe d’ac- cessibilité. 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 glo- bal à 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 re- tour 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). 3 Une technique de validation de protocoles pour les automates complexes 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. 3.1 Graphe de sauts [8] 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 3 LRA :Leaping Reachability Analysis. 5 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é. Transitions simultanément exécutables. Pour calculer les transitions simul- tanément exécutables qui rentrent dans la construction d’un graphe de sauts, nous avons besoin d’abord de définir les notions de transitions exécutables et transitions potentiellement exécutables. 0 Transitions exécutables : Une transition t = (si , µ, si ) d’une entité commu- nicante Pi est dite exécutable à l’état global G, ssi si = sGi (i.e si est l’état local de l’entité Pi à l’état global G) et t vérifie une des deux conditions suivantes : 1. t est une transition d’envoi de message et le contenu du canal Cij est inférieure à K, i.e. |Cij | < K. ou, 2. t est une transition de réception de message tel que µ = +y avec y ∈ Mi et F ront(cG ji ) = y . Autrement dit, t peut recevoir le message qui est en tête du canal cji . L’ensemble des transitions d’envoi ou de réception de messages de l’entité Pi , qui sont exécutables à l’état globale G, sont notés respectivement Xi− (G) et Xi+ (G). L’union de ces deux ensembles est noté Xi (G) = Xi− (G) ∪ Xi+ (G). L’ensemble de toutes les transitions des différentes entité communicantes du protocole qui sont exécutables à l’état G, est noté : X(G) = ∪i∈I Xi (G). Transitions potentiellement exécutables : Une transition de réception de 0 message t = (si , +y, si ) est dite potentiellement exécutable à l’état global G, ssi 0 si = sG G i et cji = ε. Une transition d’envoi de message t = (si , −x, si ), est dite potentiellement exécutable à l’état global G, ssi si = sG i et |Cij | = K ; K est 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é Pi qui sont potentiellement exécutables à l’état globale G, sont noté respectivement Pi+ (G) et Pi− (G). L’ensemble de toutes les transitions potentiellement exécutables de l’entité Pi est noté : Pi (G) = Pi− (G) ∪ Pi+ (G). Lors de la construction d’un graphe de sauts, les transitions à exécuter simul- tanément, doivent être exécutables dans le même état global et doivent apparte- nir à 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 (pro- per leap). Donc, un saut est un ensemble non vide de transitions : T ⊆ X(G), 0 0 0 tel que pour toute transition t, t ∈ T , act(t) 6= act(t ) si t 6= 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). 6 Definition 1 (Calcul de l’ensemble pleap (sauts)[7]). Soit G un état glo- bal. 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/Xi (G) =⇒ Pi (G) 6= }. L’ensemble des sauts pleap(G) est donc calculé comme suite : ( nQ o i∈W / ait(G) X i (G) si W ait(G) ⊂ I pleap(G) = (1) {{t} /t ∈ X(G)} sinon 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 l’ensemble W ait(G) est inclut dans I, l’ensemble de sauts à exécuter à partir de G (pleap(G)) sera le produit cartésien desQensembles de transitions exécutables de chaque entité Xi(G) i.e pleap(G) = { i∈W / ait(G) {Xi (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 : →l . Pour deux états glo- baux G1 = (< sG1 i >i∈I , < cG1 G2 ij >(i,j)∈L ) et G2 = (< si >i∈I , < cG2 ij >(i,j)∈L ), G1→l G2 existe, ssi il existe un ensemble de transitions T appartenant à l’en- semble 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 : G1 = Q0 →T 1 Q1 →T 2 Q2 . . . →T m Qm = G2. 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. 3.2 Construction de chemins de sauts réversibles 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. Definition 3 (état global réversible [5]). Lorsque on parcourt un graphe d’accessibilité d’une manière réversible, l’ensemble des états construit par cette opération est appelé ensemble d’états globaux réversibles. Un état global réversible G G G d’un protocole Π est noté G = (< si >i∈I , < cij >(i,j)∈L ) où si est l’état local G de l’entité Pi et cij est la séquence de messages désirés sur le canal Cij . 7 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). 0 Transition réversiblement exécutable : transition t = (si , µ, si ) ∈ 4i , est 0 0 0 G G dite réversiblement exécutable à l’état global réversible G, ssi si = si (si est l’état local de Pi à l’état global G) , et t est sous une des deux formes suivantes : 1. t est une transition d’envoi de message tel que µ = −x avec x ∈ Mi et G F ront(cij ) = x. ou, 2. t est une transition de réception de message et le contenu du canal cji est inférieure à K, i.e. |Cji | i∈I , < cij >(i,j)∈L ) et G2 = G2 G2 (< si >i∈I , < cij >(i,j)∈L ), G1→R G2 existe, ssi il existe un ensemble de transitions réversiblement exécutables T ∈ pleapR (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 di- recte 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. 3.3 Traitement des erreurs d’interblocage 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]). Un état global G = (< sG G i >i∈I , < cij >(i,j)∈L ) est dit un possible état d’interblocage ssi, ∀(i, j) ∈ L : G G cij = ε et si est un état de réception de message pour tout i ∈ I. Definition 7 (état d’interblocage [8]). Un état global G = (< sG i >i∈I , < cG ij >(i,j)∈L ) est dit état d’interblocage ssi : 9 1. ∀(i, j) ∈ L : cG G ij = ε et si 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 communi- cations 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. 3.4 Algorithme Dans cette section, nous donnons l’algorithme de notre approche de valida- tion. Pour des raisons de simplifications, nous traitons des protocoles de com- munication entre deux entités seulement. Notre algorithme peut être facilement généralisé sur une communication entre plusieurs entités. Détection des états suspects (Phase1). 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 pro- tocole (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. Confirmation des états d’interblocage (Phase2). 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 pro- tocole. 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 0 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). 10 Algorithm 1 Phase de détection des états suspects Require: Entrées :protocole Π(P1, P2) ; Pi =(Si ,S0i ,Efi ,Mi ,4i ) i∈{1,2} ; Sortie :Suspect ;//ensemble des états suspects 1: Suspect=∅ ; 2: pour chaque état de réception de message s1 dans S1 faire 3: pour chaque état de réception de message s2 dans S2 faire 4: si s1 et s2 sont des états non finaux alors 5: GS = (s1 , s2 , ε, ε) ;//générer un état suspect 6: Suspect = Suspect ∪ {GS} ; 7: finsi 8: fin pour 9: fin pour Algorithm 2 Phase de confirmation des états d’interblocage Require: Entrées :protocole Π(P1, P2) ; Pi =(Si ,S0i ,Efi ,Mi ,4i ) i∈{1,2} ; Etat global suspect GS : (s1 , s2 , ε, ε)//s1 ∈ S1, s2 ∈ S2 Sortie :Confirmation ou non de l’erreur dans l’état suspect GS ; 1: Explored = ∅ ; 2: Open = {GS} ; 3: tantque Open 6= Ø faire 4: Prendre un état global G de Open ; 5: Open = Open − {G} ; 6: Explored = Explored ∪ {G} ; 7: si G = S0 alors 8: si G.s1 est complexe ET G.s2 est complexe alors 9: retourne : GS est confirmé comme erreur d’interblocage complexe ; 10: sinon 11: si G.s1 est complexe OU G.s2 est complexe alors 12: retourne : GS est confirmé comme erreur d’interblocage hybride ; 13: sinon 14: retourne : GS est confirmé comme erreur d’interblocage simple ; 15: finsi 16: finsi 17: sinon 18: calculer pleapR (G) ; // calcul des sauts réversibles à partir de G 19: pour tout T dans pleapR (G) faire 0 20: Générer un état G par l’exécution simultané des transitions de T ; 0 21: si G ∈ / Explored alors 0 22: Open = Open ∪ G 23: finsi 24: fin pour 25: finsi 26: fin tantque 27: retourne :GS n’est pas une erreur de protocole ; 11 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. 4 Résultas d’expérimentation Pour montrer l’efficacité de notre technique, nous avons choisi de la compa- rer avec une technique de la même famille, c’est-à-dire une technique qui utilise le principe de retour arrière. La technique choisie est l’analyse d’accessibilité réversible (Reverse Reachability analysis) RRA. Cette technique a prouvée son efficacité par rapport à plusieurs d’autres techniques de validation. La compa- raison se fait sur la taille du graphe d’accessibilité généré afin de valider le pro- tocole. La taille d’un graphe d’accessibilité est mesurée par rapport au nombre d’états globaux générés et par rapport au nombre de transitions exécutées pour sa construction. Nous avons fait notre comparaison sur le même ensemble d’exemples utilisé pour valider la technique RRA. Le Tableau 1 montre la réduction apportée par notre technique sur l’ensemble des exemples de comparaison selon la variation en taille des canaux de communication. Réduction sur la taille du graphe d’accessibilité : RLRA/RRA Capacité des canaux C12=C21 Nombre d’états explorés Nombre de transitions exécutées 1 11,11% 20,54% 2 21,42% 32,20% 3 4% 12,68% 4 2,17% 6,06% 5 6,42% 7,38% Tab. 1. Réduction apportée par la technique RLRA par rapport à la technique RRA 5 Conclusion 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é. 12 Références 1. Choi, T.Y. : A structured approach to the analysis and design of finite state proto- cols. Ph.D.Thesis, School of Electrical Engineering, Georgia Institute of Technology, 1983. 2. Gouda, M.G., and Yu, Y.T. : Protocol validation by maximal progress state explo- ration. in Proceedings of ACM SIGCOMM, pp. 68-75, 1983. 3. Lin, F.J., Chu, P.M. and Liu, M.T. : Protocol verification using reachability analy- sis : the state space explosion problem and relief strategies, Computer communica- tions Review, volume 17, no.5, pp. 126-143, 1987. 4. Peng, w. and Purushothaman, S. : Data flow analysis of communicating finite state machines. ACM Transactions on Programming Languages and Systems, Vol. 13, No. 3, pp.399-442, July 1991. 5. Hung, Y.C., and Chen, G.H., ”Reverse reachability analysis : a new technique for deadlock detection on communicating finite state machines”, Softwar Practice and Experience, September, volume 23(9), pp.88-93, 1993. 6. Ozdemir, K. : Verifying the safety properties of concurrent systems via simultaneous reachability, Ph.D. Thesis, Department of CSI, University of Ottawa, 1995. 7. Hans, V.S., and Hasan, U. ; A uniform approach to tackle state explosion in verifying progress properties for networks of CFSMs*. Department of Computer Science, University of Ottawa, TR-96-13, November 1996. 8. Ozdemir, K. and Ural, H. : Protocol validation by simultaneous reachability analysis, Computer Communications, 20(9) : 772-788, 1997. 9. Tari, Z. and Arora, P. : A Communication Protocol Validation Approach based on Partial Exploration of Complex State Machines ,ICDCIT, 2007.