R´esum´e L'analyse d'accessibilit´e est g´en´eralement l'approche utilis´ee pour la validation des protocoles. Le probl`eme pos´e 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´ee Reverse Leaping Reachability Analysis (RLRA). Au lieu de parcourir tout l'espace des ´etats de protocole, notre approche explore seulement un ensemble r´eduit de cet espace afin de d´etecter les erreurs de type Interblocage. Les r´esultats d'exp´erimentation ont montr´e que notre technique permet de r´eduire la taille du graphe d'accessibilit´e de protocole est donc r´eduire le probl`eme de l'explosion combinatoire. Mots-cl´e: validation de protocoles, automate `a ´etats complexes, interblocage
Dans le domaine des Services Web, les protocoles de communication peuvent
ˆetre mod´elis´es sous forme de communication d’automates `a ´etats finis. Dans ce
mod`ele, le comportement de chaque entit´e communicante est sp´ecifi´e par un
Automate `a Etats Finis (AEF). Ces entit´es ´echangent des messages via des canaux
de communication de capacit´e limit´ee. La validation de protocoles, consiste `a
v´erifier l’absence des erreurs logiques de sp´ecification telles que les erreurs
d’interblocage et les r´eceptions non sp´ecifi´ees. L’analyse d’accessibilit´e standard est
g´en´eralement l’approche la plus utilis´ee dans le domaine de validation de
protocoles. Le principe de cette technique est l’´enum´eration de toutes les interactions
possibles entre les entit´es communicantes. Cette ´enum´eration g´en`ere des ´etats
globaux de protocole ou` chaque ´etat global donne la situation du protocole apr`es
avoir ex´ecut´e une op´eration. A la fin de cette op´eration, on obtient un graphe
d’accessibilit´e de protocole. Les erreurs de protocole, sont alors d´etect´ees par la
v´erification de chaque ´etat global composant ce graphe. L’analyse d’accessibilit´e
standard est une technique intuitive, simple et permet la d´etection de toutes les
erreurs que peut contenir une sp´ecification de protocole. Cependant, elle soufre
du probl`eme de l’explosion combinatoire. En g´en´eral, le nombre total des ´etats
globaux d’un protocole est exponentiel en terme de nombre d’entit´e composant
le protocole ainsi que le nombre d’´etat local de chaque entit´e [
L’analyse d’accessibilit´e r´eversible [
Dans cet article, nous proposons une technique de validation de protocoles mod´elis´es sous forme de Communication d’Automate d’Etats Finis Complexes (CAEFC), appel´ee RLRA (Reverse Leaping Reachability Analysis). Notre technique, permet la d´etection de toutes les erreurs de type interblocage dans une sp´ecification de protocole. En se basant sur une approche de validation avec retour arri`ere, on commence par identifier de possibles ´etats d’interblocage ensuite, valider parmi ces ´etats suspects, ceux qui pr´esentent r´eellement une erreur a` travers la recherche de chemins de retour vers la racine du graphe de protocole. Pour r´eduire le probl`eme de l’explosion combinatoire, nous introduisons les graphes de sauts (leap graphe) que nous exploitons dans la construction des chemins de retour arri`ere. Ces graphes de sauts, permettent d’´eviter le parcourt des ´etats globaux qui ne sont pas utiles dans l’analyse, ce qui apporte une r´eduction importante sur la taille du graphe `a parcourir. Pour chaque erreur confirm´ee, nous donnons aussi sa nature (simple, hybride ou complexe) selon la nature des ´etats qui pr´esentent l’erreur.
Le reste de cet article est organis´e comme suite : La prochaine section introduit le mod`ele de CAEFC. La section trois, explique notre approche de validation ainsi que les prouves formelles de son applicabilit´e. La quatri`eme section, donne les r´esultats d’exp´erimentation. La derni`ere section est une conclusion de ce travail. 2
Mod`ele de Communication d’Automates `a Etats Finis
Complexes (CAEFC)[
Un mod`ele de CAEFC introduit la notion d’´etat complexe, qui est un AEF dont certains de ses ´etats sont eux-mˆemes des AEF (internes). Les ´etats qui rentrent dans la composition d’un ´etat complexe sont appel´es ´etats internes. Le d´eveloppement des diff´erents 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`ele de Communication d’automate d’´etats finis, un protocole Π est une paire (P, L), ou` P = {Pi/i ∈ I} est l’ensemble des n entit´es communicantes du protocole et L ⊆ I × I est la relation d’incidence non r´eflexive qui identifie un ensemble non vide de canaux de communication {Cij /(i, j) ∈ L}. Chaque canal Cij est une file FIFO, born´ee et sans erreurs reliant l’entit´e Pi `a l’entit´e Pj . Chaque entit´e Pi est un automate d’´etats finis : (Si,S0i,Efi,Mi,4i) (simple ou complexe), compos´e d’un ensemble d’´etats Si , d’un ensemble d’´etats finaux Efi ,d’un alphabet de messages Mi ,d’un ensemble de transitions 4i et d’un ´etat initial S0i. L’ensemble des ´etats Si comprend des ´etats simples et des ´etats complexes. Chaque ´etat complexe doit ˆetre d´efini par un AEF. Le contenu du canal Cij , not´e 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´e Pi envoie des messages sur son canal de sortie Cij (i, j ∈ I ∧ i 6= j) et rec¸oit des messages sur ses canaux d’entr´ees Cji (i, j ∈ I ∧ i 6= j). La relation de transition 4i est d´efinie par :4i :Si × Mi → Si. Une transition t = (si, μ, s0i) ∈ Δi, d´efinie a` l’´etat local si de l’entit´e Pi, est dite transition d’envoi de message lorsque μ = −x, indiquant un envoi d’un message x (x ∈ Mi) par l’entit´e Pi sur le canal Cij . t est dite transition de r´eception de message lorsque μ = +y, indiquant une r´eception d’un message y (y ∈ Mi) par l’entit´e Pi depuis le canal Cji. Les signes - et + indiquent respectivement un envoi et une r´eception de message. Dans le cas ou` s0i est un ´etat complexe (repr´esente un AEF interne), le r´esultat de la transition va mettre l’automate interne sur sont ´etat initial, si si et aussi un ´etat complexe, la transition ne peut ˆetre ex´ecut´ee que si l’automate lui correspondant atteint sont ´etat final.
Un ´etat global G du protocole Π est repr´esent´e par une paire (< siG >i∈I , < ciGj >(i,j)∈L), ou` siG est l’´etat local de l’entit´e Pi et cijG est le contenu du canal Cij `a l’´etat global G. L’´etat global initial est not´ee G0 = (< siG0 >i∈I , < ciGj0 >(i,j)∈L), tel que siG0 = S0i et ciGj0 = ε , pour tout i ∈ I et (i, j) ∈ L.
1. Pour une transition t ∈ Δi , act(t) = i est l’indice de l’entit´e auquel appartient la transition t, 2. Pour un ensemble de transition T , act(T ) = {i ∈ I/T ∩Δi 6= ε} est l’ensemble des indices des entit´es qui ont au moins une transition dans T ; Nous d´efinissons ´egalement la fonction F ront(ciGj ) qui renvoie le message en tˆete du canal cij `a l’´etat global G.
En plus de la nature de l’erreur logique, l’utilisation des automates d’´etats complexes n´ecessite la d´efinition du type de l’erreur d´etect´ee qui peut ˆetre de type simple, lorsque chaque entit´e communicante se trouve dans un de ses ´etats simples, complexe lorsque toutes les entit´es se trouvent dans un de leurs ´etats complexes et hybride lorsque une ou plusieurs entit´es du mod`ele se trouvent dans un ´etat simple et le reste des entit´es se trouvent dans des ´etats complexes. 2.2
La validation d’un protocole revient `a faire une analyse de son graphe
d’accessibilit´e. Un graphe d’accessibilit´e donne les diff´erentes ex´ecutions possibles
du protocole, les noeuds de ce graphe sont les ´etats globaux du protocole et
les arcs sont les diff´erentes transitions (interactions) qui font pass´e le protocole
d’un ´etat global vers un autre. L’approche de validation exhaustive soufre du
probl`eme de l’explosion combinatoire qui est duˆ au grand nombre d’´etat
global `a g´en´erer pendant l’analyse. Ce probl`eme peut ˆetre r´eduit en adoptant une
approche de validation avec retour arri`ere. Cette approche est appel´ee analyse
d’accessibilit´e r´eversible (RRA )[
Une technique de validation de protocoles pour les automates complexes
Dans cette section, nous proposons une technique de validation de protocoles
qui est bas´ee sur une approche avec retour arri`ere. Dans notre approche de
retoure arri`ere, au lieu de travailler sur un graphe d’accessibilit´e standard (couvre
tout l’espace des ´etats), nous utilisons un graphe de sauts (LRA3)[
Un graphe de sauts est un graphe d’accessibilit´e r´eduit. Cette r´eduction est obtenue du fait que le passage d’un ´etat global vers un autre peut se faire via 3 LRA :Leaping Reachability Analysis. l’ex´ecution de plusieurs transitions `a la fois, ce qui permet d’´eviter de g´en´erer des ´etats interm´ediaires r´esultants de l’ex´ecution de chaque transition `a part. les transitions qui peuvent s’ex´ecuter en mˆeme temps sont appel´ees : transitions simultan´ement ex´ecutables.Ces transitions simultan´ees forme un saut dans un graphe d’accessibilit´e.
tan´ement ex´ecutables qui rentrent dans la construction d’un graphe de sauts, nous avons besoin d’abord de d´efinir les notions de transitions ex´ecutables et transitions potentiellement ex´ecutables.
Transitions ex´ecutables : Une transition t = (si, μ, s0i) d’une entit´e communicante Pi est dite ex´ecutable `a l’´etat global G, ssi si = siG (i.e si est l’´etat local de l’entit´e Pi `a l’´etat global G) et t v´erifie une des deux conditions suivantes : 1. t est une transition d’envoi de message et le contenu du canal Cij est inf´erieure `a K, i.e. |Cij | < K. ou, 2. t est une transition de r´eception de message tel que μ = +y avec y ∈ Mi et F ront(cjGi) = y . Autrement dit, t peut recevoir le message qui est en tˆete du canal cji.
L’ensemble des transitions d’envoi ou de r´eception de messages de l’entit´e Pi, qui sont ex´ecutables `a l’´etat globale G, sont not´es respectivement Xi−(G) et Xi+(G). L’union de ces deux ensembles est not´e Xi(G) = Xi−(G) ∪ Xi+(G). L’ensemble de toutes les transitions des diff´erentes entit´e communicantes du protocole qui sont ex´ecutables `a l’´etat G, est not´e : X(G) = ∪i∈I Xi(G).
Transitions potentiellement ex´ecutables : Une transition de r´eception de message t = (si, +y, s0i) est dite potentiellement ex´ecutable `a l’´etat global G, ssi si = siG et cjGi = ε. Une transition d’envoi de message t = (si, −x, s0i), est dite potentiellement ex´ecutable `a l’´etat global G, ssi si = siG et |Cij | = K ; K est la capacit´e des canaux de communication du syst`eme. L’ensemble des transitions de r´eception de message et des transitions d’envoi de message de l’entit´e Pi qui sont potentiellement ex´ecutables `a l’´etat globale G, sont not´e respectivement Pi+(G) et Pi−(G). L’ensemble de toutes les transitions potentiellement ex´ecutables de l’entit´e Pi est not´e : Pi(G) = Pi−(G) ∪ Pi+(G).
Lors de la construction d’un graphe de sauts, les transitions `a ex´ecuter
simultan´ement, doivent ˆetre ex´ecutables dans le mˆeme ´etat global et doivent
appartenir `a des entit´es du protocole qui ne disposent pas de transitions potentiellement
ex´ecutables [
bal. On note par W ait(G), l’ensemble des indices des entit´es qui disposent d’une transition potentiellement ex´ecutable `a l’´etat G. Cet ensemble est d´efinit par : W ait(G) = {i ∈ I/Xi(G) =⇒ Pi(G) 6= }. L’ensemble des sauts pleap(G) est donc calcul´e comme suite : pleap(G) = ( nQ i∈/W ait(G) Xi (G)
o {{t} /t ∈ X(G)} si W ait(G) ⊂ I sinon (1) Avant de calculer l’ensemble pleap(G) , on doit calculer l’ensemble W ait(G) pour identifier les entit´es qui disposent de transitions potentiellement ex´ecutables. Si toutes les entit´es appartiennent `a l’ensemble W ait(G) ¸ca veut dire qu’il n’y a pas de saut `a faire `a partir de G et dans ce cas la, on ex´ecute chaque transition de X(G) ind´ependamment des autres (transitions simples). Si l’ensemble W ait(G) est inclut dans I, l’ensemble de sauts `a ex´ecuter `a partir de G (pleap(G)) sera le produit cart´esien des ensembles de transitions ex´ecutables de chaque entit´e
Q Xi(G) i.e pleap(G) = { i∈/W ait(G){Xi (G)}}.
Definition 2 (transition de saut [
Soit →l∗ la fermeture transitive et r´eflexive de →l. G2 est dit accessible par l sauts depuis G1, ssi G1 → ∗ G2. Si G1 = S0 (´etat global initial du protocole), G2 est dit ˆetre accessible par saut. On d´enote par LΠ l’ensemble de tous les ´etats du protocole qui sont accessibles par sauts. Pour une s´equence d’ensemble l de sauts Ω = T 1, T 2, T 3 . . . , T m, G1 → ∗ G2 d´enote l’existence des ´etats 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 ´etats globaux qui sont accessibles par des sauts. Le calcul des transitions de sauts (pleap) se fait au niveau de chaque ´etat global, en commen¸cant de l’´etat global initial du syst`eme. 3.2
Dans ce qui suit, nous donnons les d´efinitions qui vont nous permettre de construire un graphe de sauts d’une mani`ere r´eversible.
d’accessibilit´e d’une mani`ere r´eversible, l’ensemble des ´etats construit par cette op´eration est appel´e ensemble d’´etats globaux r´eversibles. Un ´etat global r´eversible d’un protocole Π est not´e G = (< siG >i∈I , < ciGj >(i,j)∈L) ou` siG est l’´etat local de l’entit´e Pi et ciGj est la s´equence de messages d´esir´es sur le canal Cij . L’op´eration de retour arri`ere peut ˆetre vue comme une proc´edure abstraite. A partir d’un ´etat global on monte vers la racine, et dans ce cas-l`a, les transitions d’envoi de messages vont ˆetre trait´ees comme ´etant des transitions de r´eception de messages, et les transitions de r´eception de messages vont ˆetre trait´ees comme ´etant des transitions d’envoi de messages.
la construction des graphes de sauts, nous avons besoin de d´efinir les notions de transitions r´eversiblement ex´ecutables et de transitions potentiellement et r´eversiblement ex´ecutables afin de calculer les transitions simultan´ement et r´eversiblement ex´ecutables (sauts r´eversibles).
Transition r´eversiblement ex´ecutable : transition t = (si, μ, s0i) ∈ 4i , est dite r´eversiblement ex´ecutable `a l’´etat global r´eversible G, ssi s0i = s0iG (s0iG est l’´etat local de Pi `a l’´etat 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
F ront(ciGj ) = x. ou, 2. t est une transition de r´eception de message et le contenu du canal cji est inf´erieure `a K, i.e. |Cji| <K.
L’ensemble des transitions d’envoi et de r´eception de messages, qui sont r´eversiblement ex´ecutables `a l’´etat global r´eversible G, sont not´es XR−(G) et XR+(G) respeci i tivement. L’union de ces deux ensembles est not´e XiR(G) = XR−(G) ∪ XR+(G). i i L’ensemble de toutes les transitions du protocole, qui sont r´eversiblement ex´ecutables a` l’´etat G, est not´e : XR(G) = ∪i∈I XiR(G).
Transition potentiellement et r´eversiblement ex´ecutable : Une transition de r´eception de message t = (si, +y, s0i), avec y ∈ Mi , est dite potentiellement et r´eversiblement ex´ecutable `a l’´etat global r´eversible G, ssi s0i = s0iG et |Cji| =K ; K est la capacit´e des canaux de communication du syst`eme. Une transition d’envoi de message t = (si, −x, s0i), avec x ∈ Mi , est dite potentiellement et r´eversiblement ex´ecutable `a l’´etat global G, ssi s0i = s0iG et ciGj = ε. Les ensembles des transitions de r´eception de messages et des transitions d’envoi de messages de l’entit´e Pi, qui sont potentiellement et r´eversiblement ex´ecutables `a l’´etat global G, sont not´es PiR+(G) et PiR−(G) respectivement. On note PiR(G) = PiR−(G) ∪ PiR+(G).
Comme pour la construction d’un graphe de sauts, la construction d’un graphe de sauts r´eversibles se fait par le calcul des transitions simultan´ement et r´eversiblement ex´ecutables, ces transitions doivent ˆetre ex´ecutables dans le mˆeme ´etat global r´eversible et doivent appartenir `a des entit´es du protocole qui ne disposent pas de transitions potentiellement et r´eversiblement ex´ecutables. Un ensemble de telles transitions est appel´e sauts r´eversibles, not´e pleapR (reverse proper leap). Donc, un saut r´eversible est un ensemble non vide de transitions : T ⊆ XR(G), tel que pour toute transition t, t0 ∈ T , act(t) 6= act(t0 ) si t 6= t0 (i.e T contient au plus une transition r´eversiblement ex´ecutable de chaque entit´e). Les diff´erents ensembles T , construits `a l’´etat global r´eversible G, forment un ensemble de sauts r´eversibles not´e pleapR(G).
Nous donnons dans ce qui suit la d´efinition formelle de l’ensemble des sauts r´eversibles pleapR.
On d´efinit l’ensemble des entit´es qui disposent d’une transition potentiellement et r´eversiblement ex´ecutable `a l’´etat G par : W aitR(G) = {i ∈ I/XiR(G) =⇒ PiR(G) 6= }. L’ensemble pleapR(G) est calcul´e comme suite : pleapR(G) = ( nQ
i∈/W aitR(G) XiR(G) {t} /t ∈ XR(G) o si
W aitR(G) ⊂ I sinon (2) Avant de calculer l’ensemble pleapR(G), on doit calculer l’ensemble W aitR(G) pour identifier les entit´es qui disposent de transitions potentiellement et r´eversiblement ex´ecutables. Si toutes les entit´es appartiennent `a l’ensemble W aitR(G) ¸ca veut dire qu’il n’y a pas de saut r´eversible `a ex´ecuter `a partir de G, et dans ce cas la, on ex´ecute chaque transition de XR(G) ind´ependamment des autres (simple transition). Si l’ensemble W aitR(G) est inclut dans I, l’ensemble de sauts r´eversibles pleapR(G) sera le produit cart´esien des ensembles de transitions r´eversiblement Q ex´ecutables de chaque entit´e(XiR(G)), i.e pleapR(G) = { i∈/W aitR(G){XiR (G)}}.
est une relation binaire →R sur un ensemble d’´etats globaux r´eversibles. Pour deux ´etats globaux r´eversibles G1 = (< siG1 >i∈I , < ciGj1 >(i,j)∈L) et G2 = (< siG2 >i∈I , < ciGj2 >(i,j)∈L), G1→RG2 existe, ssi il existe un ensemble de transitions r´eversiblement ex´ecutables T ∈ pleapR(G1), tel que l’ex´ecution des transitions de T `a partir de G1 donne l’´etat global G2. La relation de transition G1 →R G2 signifie que l’´etat global G2 est obtenu d’une mani`ere r´eversible directe depuis l’´etat global G1. Soit →R∗ la fermeture transitive et r´eflexive de →R, on dit que l’´etat G2 est accessible par saut r´eversible de puis G1, ssi G1 →R∗ G2. Le chemin qui relie G1 vers G2 est alors appel´e : chemin de sauts r´eversibles de G1 vers G2. 3.3
Dans cette section, nous expliquons l’utilisation des sauts r´eversibles pour la d´etection des erreurs d’interblocage.
Definition 6 (´etat suspect d’interblocage [
Un ´etat global est dit ´etat d’interblocage lorsque tous les canaux de communications dans cet ´etat sont vides et toutes les entit´es du protocole sont dans un ´etat de r´eception de messages.
Nous donnons ci-dessous, le th´eor`eme principal de notre proposition, qui nous permettra d’utiliser les chemins de sauts r´eversibles afin de d´etecter les erreurs logiques de type interblocage.
Theorem 1. Soit P i = (P, L) un protocole et soit GS un ´etat global suspect d’interblocage.
L’´etat suspect d’inter blocage GS, est confirm´e comme ´etat d’inter blocage ssi, l’´etat global initial du protocole G0 est accessible par un chemin de sauts r´eversibles a` partir de l’´etat suspect GS.
On se basant sur le th´eor`eme 1, la d´etection des ´etats d’interblocage, peut ˆetre faite par une v´erification de l’accessibilit´e par sauts r´eversibles de l’´etat initial du syst`eme en partant d’un ´etat suspect. 3.4
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´es seulement. Notre algorithme peut ˆetre facilement g´en´eralis´e sur une communication entre plusieurs entit´es.
Les ´etats suspects d’interblocage sont obtenus par une combinaison, des ´etats locaux de r´eception de messages, des diff´erentes entit´es communicantes du protocole (D´efinition 6). Cette phase est impl´ement´ee par l’Algorithme 1 du calcul d’´etats suspects.
Le test de la ligne 4 de l’algorithme sert `a ´ecarter les ´etats locaux qui sont finaux car un ´etat global final ne peur ˆetre ´etat d’interblocage.
Afin de confirmer l’existence d’une erreur dans un ´etat suspect GS, l’algorithme effectue une recherche d’un chemin de sauts r´eversibles vers l’´etat initial du protocole.
Cette phase est donn´ee sur l’Algorithme 2. L’ensemble Explored est utilis´e pour marquer les ´etats globaux qui sont d´eja` trait´es (v´erifi´es). Chaque nouvel ´etat global n’appartenant pas `a Explored, sera mis dans Open afin de le traiter dans la prochaine it´eration (ligne 20-21-22). A partir de chaque ´etat global G0 (non trait´e), nous calculons tous les ensembles des transitions simultan´ement ex´ecutable (T ) de cet ´etat global, par l’utilisation de la d´efinition 4 (ligne 18).
Algorithm 2 Phase de confirmation des ´etats d’interblocage Pour chaque T obtenu et qui est un saut r´eversible, nous g´en´erons un nouvel ´etat global. L’algorithme continue son ex´ecution jusqu’`a ce que soit l’´etat initial est atteint, et dans ce cas la l’erreur logique est confirm´ee dans l’´etat suspect GS, soit il ne reste plus d’´etat `a explorer et donc l’erreur logique est ´ecart´ee. Les lignes de code de 7 `a 16 permettent d’identifier le type de l’erreur d´etect´ee (simple, hybride ou complexe), selon la nature des ´etats locaux composant l’´etat de l’erreur. 4
R´esultas d’exp´erimentation
Pour montrer l’efficacit´e de notre technique, nous avons choisi de la comparer avec une technique de la mˆeme famille, c’est-a`-dire une technique qui utilise le principe de retour arri`ere. La technique choisie est l’analyse d’accessibilit´e r´eversible (Reverse Reachability analysis) RRA. Cette technique a prouv´ee son efficacit´e par rapport `a plusieurs d’autres techniques de validation. La comparaison se fait sur la taille du graphe d’accessibilit´e g´en´er´e afin de valider le protocole. La taille d’un graphe d’accessibilit´e est mesur´ee par rapport au nombre d’´etats globaux g´en´er´es et par rapport au nombre de transitions ex´ecut´ees pour sa construction.
Nous avons fait notre comparaison sur le mˆeme ensemble d’exemples utilis´e pour valider la technique RRA. Le Tableau 1 montre la r´eduction apport´ee par notre technique sur l’ensemble des exemples de comparaison selon la variation en taille des canaux de communication.
Capacit´e des canaux
C12=C21 1 2 3 4 5
R´eduction sur la taille du graphe d’accessibilit´e : RLRA/RRA Nombre d’´etats explor´es 11,11% 21,42%
4% 2,17% 6,42%
Nombre de transitions ex´ecut´ees 20,54% 32,20% 12,68% 6,06% 7,38%
Dans cet article, nous avons propos´e une technique de validation de protocoles bas´ee sur une approche de validation avec retour arri`ere. Pour rendre l’analyse plus efficace, nous avons optimis´e l’op´eration de construction des chemins de retour arri`ere. 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’´eviter de parcourir des ´etats qui ne sont pas utiles dans l’analyse, ce qui nous a permet de r´eduire consid´erablement la taille du graphe d’accessibilit´e. R´ef´erences