=Paper=
{{Paper
|id=Vol-547/paper-41
|storemode=property
|title=Une technique de validation de protocoles basée sur une exploration avec retour arrière des automates complexes
|pdfUrl=https://ceur-ws.org/Vol-547/72.pdf
|volume=Vol-547
|dblpUrl=https://dblp.org/rec/conf/ciia/ZoubeyrTT09
}}
==Une technique de validation de protocoles basée sur une exploration avec retour arrière des automates complexes==
https://ceur-ws.org/Vol-547/72.pdf
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.