4 L'étude de convergence de systèmes dynamiques discrets est simple à vérifier
5 pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies
6 pseudo périodiques pour les modes unaires et généralisées, le problème
7 se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones
8 et mixes prenant de plus en compte les délais.
10 Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement
11 ont déjà été présentées~\cite{BM99,BCV02}.
12 Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un résultat
13 formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,
14 cela ne permet que donner une intuition de convergence, pas une preuve.
15 Autant que nous sachions, aucune démarche de preuve formelle automatique
16 de convergence n'a jamais été établie.
17 Dans le travail théorique~\cite{Cha06}, Chandrasekaran a montré que les itérations asynchrones sont convergentes
18 si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode
19 automatique pour construire cette fonction.
21 Un outil qui construirait automatiquement toutes
22 les transitons serait le bienvenu.
23 Pour peu qu'on établisse la preuve de correction et de complétude de la
24 démarche, la convergence du réseau discret ne repose alors que sur le verdict
26 Cependant, même pour des réseaux discrets à peu d'éléments,
27 le nombre de configurations induites explose rapidement.
28 Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}
29 sont des classes d'outils qui addressent le problème de vérifier automatiquement
30 qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion
31 combinatoire, ces outils appliquent des méthodes d'ordre partiel, d'abstraction,
32 de quotientage selon une relation d'équivalence.
34 Ce chapitre montre comment nous simulons
35 des réseaux discrets selon toutes les sortes d'itérations pour établir
36 formellement leur convergence (ou pas).
37 Nous débutons par un exemple et faisons quelques rappels sur
38 le langage PROMELA qui est le langage du model-checker
39 SPIN~\cite{Hol03} (\Sec{sec:spin:promela}).
40 Nous présentons ensuite la démarche de traduction
41 de réseaux discrets dans PROMELA (\Sec{sec:spin:translation}).
42 Les théorèmes de correction et de complétude de la démarche
43 sont ensuite donnés à la (\Sec{sec:spin:proof}).
44 Des données pratiques comme la complexité et des synthèses d'expérimentation
45 sont ensuite fournies (\Sec{sec:spin:practical}).
53 %\section{Exemple jouet}
58 \subfigure[Fonction à itérer]{
61 f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3 \\
62 f_2(x_1,x_2,x_3) & = & x_1 + \overline{x_3} \\
63 f_3(x_1,x_2,x_3) & = & x_2.x_3
70 \subfigure[Graphe d'intéraction]{
71 \includegraphics[width=4cm]{images/xplCnxMc.eps}
72 \label{fig:xplgraph:inter:mc}
75 \caption{Exemple pour SDD $\approx$ SPIN.}
81 On considère un exemple à trois éléments dans $\Bool$.
82 Chaque configuration est ainsi un élement de $\Bool^3$, \textit{i.e.},
83 un nombre entre 0 et 7.
84 La \Fig{fig:map} précise la fonction $f$ considérée et
85 la \Fig{fig:xplgraph:inter:mc} donne son graphe d'intéraction.
93 On peut facilement vérifier que toutes les itérations synchrones initialisées
94 avec $x^0 \neq 7$ soit $(111)$
95 convergent vers $2$ soit $(010)$; celles initialisées avec
97 Pour les mode unaires ou généralisés avec une
98 stratégie pseudo périodique, on a des comportements qui dépendent
99 de la configuration initiale:
101 \item initialisée avec 7, les itérations restent en 7;
102 \item initialisée avec 0, 2, 4 ou 6 les itérations convergent vers 2;
103 \item initialisées avec 1, 3 ou 5, les itérations convergent vers un des
104 deux points fixes 2 ou 7.
112 \section{Rappels sur le langage PROMELA}
113 \label{sec:spin:promela}
115 Cette section rappelle les éléments fondamentaux du langage PROMELA (Process Meta Language).
116 On peut trouver davantage de détails dans~\cite{Hol03,Wei97}.
127 bool X [N]; bool Xp [N]; int mods [N];
128 typedef vals{bool v [N]};
131 typedef a_send{chan sent[N]=[d_0] of {bool}};
134 chan unlock_elements_update=[1] of {bool};
135 chan sync_mutex=[1] of {bool};
138 \caption{Declaration des types de la traduction.}
139 \label{fig:arrayofchannels}
143 % Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
144 % \texttt{short} et \texttt{int}.
146 on peut déclarer des tableaux à une dimension
147 ou des nouveaux types de données (introduites par le mot clef
148 \verb+typedef+). % Ces derniers sont utilisés
149 % pour définir des tableaux à deux
153 Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des
154 déclarations de variables qui servent dans l'exemple de ce chapitre.
157 \item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre
158 $n$ d'éléments et le délais maximum $\delta_0$;
159 \item les deux tableaux (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes;
160 les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $x_{i+1}$
161 d'un système dynamique discret;
162 elles mémorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour;
163 il suffit ainsi de comparer \verb+X+ et \verb+Xp+ pour constater si $x$ à changé ou pas;
164 \item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'itération
165 en cours; cela correspond naturellement à l'ensemble des éléments $s^t$;
166 \item le type de données structurées \verb+vals+ et le tableau de tableaux
167 \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$
168 pour l'itération au temps $t$.
169 %(en d'autres termes, utile lors du calcul de $x^{t}$).
173 % Puisque le décalage d'un indices ne change pas fondamentalement
174 % le comportement de la version PROMELA par rapport au modèle initial
175 % et pour des raisons de clarté, on utilisera par la suite la même
176 % lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour PROMELA:
177 % \texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire.
179 Déclarée avec le mot clef \verb+chan+,
180 une donnée de type \texttt{channel} permet le
181 transfert de messages entre processus dans un ordre FIFO.
182 % Elles serait suivi par sa capacité
183 % (qui est constante), son nom et le type des messages qui sont stockés dans ce canal.
184 Dans l'exemple précédent, on déclare successivement:
186 \item un canal \verb+sent+ qui vise à mémoriser \verb+d_0+ messages de type
187 \verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+
188 éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $x_j$;
189 Il permet donc de temporiser leur emploi par d'autres elements $i$.
190 \item les deux canaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant
191 chacun un message booléen et utilisé ensuite comme des sémaphores.
195 %\subsection{PROMELA Processes}
196 Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurrence
197 au sein de systèmes. Un process est instancié soit immédiatement
198 (lorsque sa déclaration est préfixée
199 par le mot-clef \verb+active+) ou bien au moment de l'exécution de l'instruction
201 Parmi tous les process, \verb+init+ est le process initial qui permet
202 d'initialiser les variables, lancer d'autres process\ldots
205 Les instructions d'affectation sont interprétées usuellement.
206 Les canaux sont concernés par des instructions particulières d'envoi et de
207 réception de messages. Pour un canal
208 \verb+ch+, ces instructions sont respectivement notées
209 \verb+ch ! m+ et \verb+ch ? m+.
210 L'instruction de réception consomme la valeur en tête du canal \verb+ch+
211 et l'affecte à la variable \verb+m+ (pour peu que \verb+ch+ soit initialisé et non vide).
212 De manière similaire, l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal
213 \verb+ch+ (pour peu que celui-ci soit initialisé et non rempli).
214 Dans les cas problématiques, canal non initialisé et vide pour une réception ou bien rempli pour un envoi,
215 le processus est bloqué jusqu'à ce que les conditions soient remplies.
217 La structures de contrôle \verb+if+ (resp. \verb+do+) définit un choix non déterministe
218 (resp. une boucle non déterministe). Que ce soit pour la conditionnelle ou la boucle,
219 si plus d'une des conditions est établie, l'ensemble des instructions correspondantes
220 sera choisi aléatoirement puis exécuté.
222 Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init},
223 une boucle de taille $N$ initialise aléatoirement la variable globale de type tableau \verb+Xp+.
224 Ceci permet par la suite de vérifier si les itérations sont convergentes pour n'importe
225 quelle configuration initiale $x^{(0)}$.
229 Pour chaque élément $i$, si les itérations sont asynchrones
231 \item on stocke d'abord la valeur de \verb+Xp[i]+ dans chaque \verb+Xd[j].v[i]+
232 puisque la matrice $s^0$ est égale à $(0)$,
233 \item puis, la valeur de $i$ (représentée par \verb+Xp[i]+) devrait être transmise
234 à $j$ s'il y a un arc de $i$ à $j$ dans le graphe d'incidence. Dans ce cas,
235 c'est la fonction \verb+hasnext+ (détaillée à la~\Fig{fig:spin:hasnext})
236 qui mémorise ce graphe
237 en fixant à \texttt{true} la variable \verb+is_succ+, naturellement et à
238 \texttt{false} dans le cas contraire.
239 Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+.
243 \begin{minipage}[h]{.32\linewidth}
247 int i=0; int j=0; bool is_succ=0;
258 ::j< N -> Xd[j].v[i]=Xp[i]; j++;
266 ::(i!=j && is_succ==1) ->
267 channels[i].sent[j] ! Xp[i];
268 ::(i==j || is_succ==0) -> skip;
278 \caption{Process init.}\label{fig:spin:init}
280 \begin{minipage}[h]{.32\linewidth}
283 active proctype scheduler(){
285 ::sync_mutex ? 1 -> {
297 unlock_elements_update ! 1;
303 \caption{Process scheduler pour la stratégie pseudo pérodique.
304 \label{fig:scheduler}}
306 \begin{minipage}[h]{.30\linewidth}
311 :: i==0 && j ==0 -> is_succ = 1
312 :: i==0 && j ==1 -> is_succ = 1
313 :: i==0 && j ==2 -> is_succ = 0
314 :: i==1 && j ==0 -> is_succ = 1
315 :: i==1 && j ==1 -> is_succ = 0
316 :: i==1 && j ==2 -> is_succ = 1
317 :: i==2 && j ==0 -> is_succ = 1
318 :: i==2 && j ==1 -> is_succ = 1
319 :: i==2 && j ==2 -> is_succ = 1
324 \caption{Codage du graphe d'intéraction de $f$.
325 \label{fig:spin:hasnext}}
332 \section{Du système booléen au modèle PROMELA}
333 \label{sec:spin:translation}
334 Les éléments principaux des itérations asynchrones rappelées à l'équation
335 (\ref{eq:async}) sont la stratégie, la fonctions et la gestion des délais.
336 Dans cette section, nous présentons successivement comment chacune de
337 ces notions est traduite vers un modèle PROMELA.
340 \subsection{La stratégie}\label{sub:spin:strat}
341 Regardons comment une stratégie pseudo périodique peut être représentée en PROMELA.
342 Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler})
343 est iterrativement appelé pour construire chaque $s^t$ représentant
344 les éléments possiblement mis à jour à l'itération $t$.
346 Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore
347 \verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis
348 aléatoirement (grâce à $n$ choix successifs) et sont mémorisés dans le tableau
349 \verb+mods+, dont la taille est \verb+ar_len+.
350 Dans la séquence d'exécution, le choix d'un élément mis à jour est directement
351 suivi par des mises à jour: ceci est réalisé grâce à la modification de la valeur du sémaphore
352 \verb+unlock_elements_updates+.
354 \subsection{Itérer la fonction $f$}\label{sub:spin:update}
355 La mise à jour de l'ensemble $s^t=\{s_1,\ldots, s_m\}$ des éléments qui constituent la stratégie
356 $(s^t)^{t \in \Nats}$ est implantée à l'aide du process \verb+update_elems+ fourni à la
357 {\sc Figure}~\ref{fig:proc}.
358 Ce processus actif attend jusqu'à ce qu'il soit débloqué par le process
359 \verb+scheduler+ à l'aide du sémaphore \verb+unlock_elements_update+.
360 L'implantation se déroule en cinq étapes:
363 \begin{minipage}[b]{.32\linewidth}
370 :: countu == N -> break ;
372 X[countu] = Xp[countu];
378 \caption{Sauvegarde de l'état courant}\label{fig:spin:sauve}
379 \end{minipage}\hfill%
380 \begin{minipage}[b]{.32\linewidth}
383 active proctype update_elems(){
385 ::unlock_elements_update ? 1 ->
394 ::count == ar_len -> break;
408 \caption{Mise à jour des éléments.}\label{fig:proc}
409 \end{minipage}\hfill%
412 \begin{minipage}[b]{.33\linewidth}
418 (Xs[j].v[0] & !Xs[j].v[1])
420 ::j==1 -> Xp[1] = Xs[j].v[0]
422 ::j==2 -> Xp[2] = Xs[j].v[1]
428 \caption{Application de la fonction $f$.}\label{fig:p}
434 \item elle commence en mettant à jour la variable \texttt{X} avec les valeurs de \texttt{Xp} dans la fonction \texttt{update\_X},~\Fig{fig:spin:sauve}
435 \item elle mémorise dans \texttt{Xd} la valeurs disponible pour chaque élément grâce à la fonction \texttt{fetch\_values}; cette fonction est détaillée
436 dans la section suivante;
437 \item une boucle %sur les \texttt{ar\_len} éléments qui peuvent être modifiés
438 met à jour iterrativement la valeur de $j$ (grâce à l'appel de fonction \texttt{f(j)})
439 pour peu que celui-ci doive être modifié, \textit{i.e.}, pour peu qu'il soit renseigné dans
440 \texttt{mods[count]}; le code source de \texttt{F} est donné en {\sc Figure}~\ref{fig:p} et est une
441 traduction directe de l'application $f$;
442 \item les nouvelles valeurs des éléments \texttt{Xp} sont symboliquement
443 envoyés aux autres éléments qui en dépendent grâce à la fonction
444 \texttt{diffuse\_values(Xp)}; cette dernière fonction est aussi détaillée
445 dans la section suivante;
446 \item finalement, le process informe le scheduler de la fin de la tâche
447 (au travers du sémaphore \texttt{sync\_mutex}).
457 \subsection{Gestion des délais}\label{sub:spin:vt}
458 Cette section montre comment les délais inhérents au mode asynchrone sont
459 traduits dans le modèle PROMELA grâce à deux
460 fonctions \verb+fetch_values+ et \verb+diffuse_values+.
461 Celles-ci sont données en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast},
462 qui récupèrent et diffusent respectivement les valeurs des elements.
465 \begin{minipage}[h]{.475\linewidth}
468 inline fetch_values(){
471 :: countv == ar_len -> break ;
472 :: countv < ar_len ->
476 :: (i == N) -> break;
477 :: (i < N && i == j) -> {
480 :: (i < N && i != j) -> {
485 nempty(channels[i].sent[j]) ->
486 channels[i].sent[j] ?
496 \caption{Récupérer les valeurs des elements\label{fig:val}}
497 \end{minipage}\hfill%
498 \begin{minipage}[h]{.475\linewidth}
501 inline diffuse_values(values){
504 :: countb == ar_len -> break ;
505 :: countb < ar_len ->
509 :: (i == N) -> break;
510 :: (i < N && i == j) -> i++;
511 :: (i < N && i != j) -> {
516 nfull(channels[j].sent[i]) ->
517 channels[j].sent[i] !
527 \caption{Diffuser les valeurs des elements}\label{fig:broadcast}
531 La première fonction met à jour le tableau \verb+Xd+ requis pour les éléments
532 qui doivent être modifiés.
533 Pour chaque élément dans \verb+mods+, identifié par la variable
534 $j$, la fonction récupère les valeurs des autres éléments (dont le libellé est $i$)
538 \item puisque $i$ connaît sa dernière valeur (\textit{i.e.}, $D^t_{ii}$ est toujours $t$)
539 \verb+Xd[i].v[i]+ est donc \verb+Xp[i]+;
540 \item sinon, il y a deux sous cas qui peuvent peuvent potentiellement modifier la valeur
541 que $j$ a de $i$ (et qui peuvent être choisies de manière aléatoire):
543 \item depuis la perspective de $j$ la valeur de $i$ peut ne pas avoir changé (
544 c'est l'instruction \verb+skip+) ou n'est pas utile; ce dernier cas apparaît
545 lorsqu'il n'y a pas d'arc de $i$ à $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque
546 la valeur de \verb+is_succ+ qui est calculée par \verb+hasnext(i,j)+ est 0;
547 dans ce cas, la valeur de \verb+Xd[j].v[i]+ n'est pas modifiée;
548 \item sinon, on affecte à \verb+Xd[j].v[i]+ la valeur mémorisée
549 dans le canal \verb+channels[i].sent[j]+ (pour peu que celui-ci ne soit pas vide).
553 Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonction \verb+diffuse_values+. L'objectif de cette fonction
554 est de stocker les valeurs de $x$ (représenté
555 dans le modèle par \verb+Xp+) dans le canal \verb+channels+.
556 Il permet au modèle-checker SPIN d'exécuter
557 le modèle PROMELA comme s'il pouvait y avoir des délais entre processus
558 Il y a deux cas différents pour la valeur de $X_{j}$:
560 \item soit elle est \og perdue\fg{}, \og oubliée\fg{} pour permettre à $i$ de ne pas tenir compte d'une
561 des valeurs de $j$; ce cas a lieu soit lors de l'instruction \verb+skip+ ou lorsqu'il
562 n'y a pas d'arc de $j$ à $i$ dans le graphe d'incidence;
563 \item soit elle est mémorisée dans le canal \verb+channels[j].sent[i]+ (pour peu que celui-ci ne soit pas plein).
566 L'introduction de l'indéterminisme à la fois dans les fonctions \verb+fetch_values+
567 et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était
568 présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer
569 la valeur $x_i^{(t)}$ sans considérer la valeur $x_i^{(t-1)}$.
570 De manière duale, si le non déterminisme était uniquement
571 utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait
572 mise dans le canal, elle serait immédiatement consommée, ce qui est contradictoire avec la notion de
575 % \subsection{Discussion}
576 % A coarse approach could consist in providing one process for each element.
577 % However, the distance with the mathematical model given in \Equ{eq:async} of
578 % such a translation would be larger than the method presented along these lines.
579 % It induces that it would be harder to prove the soundness and completeness of
580 % such a translation. For that reason we have developed a PROMELA model that is
581 % as close as possible to the mathematical one.
583 % Notice furthermore that PROMELA is an imperative language which
584 % often results in generating intermediate states
585 % (to execute a matrix assignment for
587 % The use of the \verb+atomic+ keyword allows the grouping of
588 % instructions, making the PROMELA code and the DDN as closed as possible.
590 \subsection{Propriété de convergence universelle}
591 Il reste à formaliser dans le model checker SPIN le fait que les
592 itérations d'un système
593 dynamique à $n$ éléments est universellement convergent.
595 Rappelons tout d'abord que les variables \verb+X+ et \verb+Xp+
596 contiennent respectivement la valeur de $x$ avant et après la mise à jour.
597 Ainsi, si l'on effectue une initialisation non déterministe de
598 \verb+Xp+ et si l'on applique une stratégie pseudo périodique,
599 il est nécessaire et suffisant
600 de prouver la formule temporelle linéaire (LTL) suivante:
602 \diamond (\Box \verb+Xp+ = \verb+X+)
605 où les opérateur $\diamond$ et $\Box$ ont
606 la sémantique usuelle, à savoir
607 respectivement {\em éventuellement} et {\em toujours} dans les chemins suivants.
608 On note que cette propriété, si elle est établie, garantit
609 la stabilisation du système.
610 Cependant elle ne donne aucune métrique quant à
611 la manière dont celle-ci est obtenue.
612 En particulier, on peut converger très lentement ou le système peut même
613 disposer de plusieurs points fixes.
617 \section{Correction et complétude de la démarche}\label{sec:spin:proof}
619 Cette section présente les théorèmes
620 de correction et de complétude de l'approche.
621 (Théorèmes~\ref{Theo:sound} et~\ref{Theo:completeness}).
622 Toutes les preuves sont déplacées en
623 annexes~\ref{anx:promela}.
626 \begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
629 Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.
631 la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible, alors
632 les itérations de $\phi$ sont universellement convergentes.
636 \begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete}
637 \label{Theo:completeness}
639 Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction. Si $\psi$ ne vérifie pas
640 la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
641 alors les itérations de $\phi$ ne sont pas universellement convergentes.
649 \section{Données pratiques}
650 \label{sec:spin:practical}
651 Cette section donne tout d'abord quelques mesures de complexité de l'approche
652 puis présente ensuite les expérimentations issues de ce travail.
654 \begin{theorem}[Nombre d'états ]
655 Soit $\phi$ un modèle de système dynamique discret à $n$ éléments, $m$
656 arcs dans le graphe d'incidence
657 et $\psi$ sa traduction en PROMELA. Le nombre de configurations
658 de l'exécution en SPIN de $\psi$ est bornée par $2^{m(\delta_0+1)+n(n+2)}$.
661 Une configuration est une valuation des variables globales.
662 Leur nombre ne dépend que de celles qui ne sont pas constantes.
664 Les variables \verb+Xp+ et \verb+X+ engendrent $2^{2n}$ états.
666 \verb+Xs+ génère $2^{n^2}$ états.
667 Chaque canal de \verb+array_of_channels+
668 peut engendrer $1+2^1+\ldots+2^{\delta_0}= 2^{\delta_0+1}-1$ états.
669 Puisque le nombre d'arêtes du graphe d'incidence est $m$,
670 il y a $m$ canaux non constants, ce qui génère approximativement $2^{m(\delta_0+1)}$ états.
671 Le nombre de configurations est donc borné par $2^{m(\delta_0+1)+n(n+2)}$.
672 On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de $n$,
674 %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
678 La méthode détaillée ici a pu être appliquée sur l'exemple
679 pour prouver formellement sa convergence universelle.
681 On peut remarquer que SPIN n'impose l'équité faible qu'entre les process
682 alors que les preuves des deux théorèmes précédentes reposent sur le fait que
683 celle-ci est établie dès qu'un choix indéterministe est effectué.
684 Naïvement, on pourrait considérer comme hypothèse la formule suivante
685 chaque fois qu'un choix indéterministe se produit entre $k$ événements
686 respectivement notés $l_1$, \ldots $l_k$:
688 \Box \diamond (l == l_0) \Rightarrow
689 ((\Box \diamond (l== l_1)) \land \ldots \land (\Box \diamond (l == l_k)))
692 où le libellé $l_0$ dénote le libellé de la ligne précédent
693 le choix indéterministe.
694 Cette formule traduit exactement l'équité faible.
695 Cependant en raison de l'explosion de la taille du produit entre
696 l'automate de Büchi issu de cette formule et celui issu du programme PROMELA,
697 SPIN n'arrive pas à vérifier si la convergence universelle est établie
698 ou non sur des exemples
699 simples.%\JFC{faire référence à un tel exemple}.
701 Ce problème a été pratiquement résolu en laissant SPIN
702 générer toutes les traces d'exécution,
703 même celles qui ne sont pas équitables,
704 puis ensuite vérifier la propriété de convergence sur toutes celles-ci.
705 Il reste alors à interpréter les résultats qui peuvent être de deux types. Si la convergence est
706 établie pour toutes les traces, elle le reste en particulier pour les traces équitables.
707 Dans le cas contraire on doit analyser le contre exemple produit par SPIN.
710 % \JFC{Reprendre ce qui suit}
711 % Experiments have shown that all the iterations of the running example are
712 % convergent for a delay equal to 1 in less than 10 min.
713 % The example presented in~\cite{abcvs05} with five elements taking boolean
714 % values has been verified with method presented in this article.
715 % Immediately, SPIN computes a counter example, that unfortunately does not
716 % fulfill fairness properties. Fair counter example is obtained
718 % All the experimentation have been realized in a classic desktop computer.
722 La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement
723 leur convergence ou leur divergence (\Fig{fig:exp:promela})
725 Dans ces expériences, les délais ont été bornés par $\delta_0=10$.
726 Dans ce tableau, $P$ est vrai ($\top$) si et seulement si la convergence
728 est établie et faux ($\bot$) sinon. Le nombre $M$ est
729 la taille de la mémoire consommée (en MB) et
730 $T$ est le temps d'exécution sur un Intel Centrino Dual Core 2 Duo @1.8GHz avec 2GB de mémoire vive
731 pour établir un verdict.
737 \subfigure[Sans délais]{
738 \begin{tabular}{|*{7}{c|}}
740 \multicolumn{1}{c|}{ }
741 &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Généralisées} \\
743 \multicolumn{1}{c|}{ }&
748 $\top$ & 2.7 & 0.01s &
749 $\bot$ & 369.371 & 0.509s \\
752 $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
753 $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
756 $\top$ & 36.7 & 12s & % BM99_sync_para.spin
757 $\top$ & & \\ % BM99_sync_chao.spin
763 \subfigure[Avec délais]{
764 \begin{tabular}{|*{13}{c|}}
766 \multicolumn{1}{c|}{ }
767 &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement borné} \\
769 \multicolumn{1}{c|}{ }
770 &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} &
771 \multicolumn{3}{|c|} {Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} \\
773 \multicolumn{1}{c|}{ }
780 $\top$ & 409 & 1m11s&
781 $\bot$ & 370 & 0.54 &
783 $\bot$ & 370 & 0.51s \\
786 &$\bot$ & 2.5 & 0.001s % RC07_async_mixed.spin
787 &$\bot$ & 2.5 & 0.01s % RC07_async_mixed_all.spin
788 &$\bot$ & 2.5 & 0.01s % RC07_async.spin
789 &$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin
792 &$\top$ & & %BM99_mixed_para.spin
793 &$\top$ & & % RC07_async_mixed_all.spin
794 &$\bot$ & & % RC07_async.spin
795 &$\bot$ & & \\ % RC07_async_all.spin
798 \label{fig:async:exp}
802 \caption{Résultats des simulations Promela des SDDs}\label{fig:exp:promela}
807 L'exemple \textit{RE} est l'exemple de ce chapitre,
808 \cite{RC07} concerne un réseau composé de deux gènes
809 à valeur dans $\{0,1,2\}$,
810 AC2D est un automate cellulaire avec 9 elements prenant des
811 valeurs booléennes en fonction de
813 \cite{BM99} consiste en 10 process
814 qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche
818 L'exemple \textit{RE} a été prouvé comme universellement convergent.
819 \JFC{statuer sur AC2D}
820 Comme la convergence n'est déjà pas établie pour les itérations synchrones
821 de~\cite{RC07}, il en est donc
822 de même pour les itérations asynchrones.
823 La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation
824 de la convergence. Celle-ci correspond à une stratégie périodique qui répète
825 $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et débute avec $x=(0,0)$.
826 En raison de la dépendance forte entre les éléments
828 $\delta_0$ est réduit à 1. Cela aboutit cependant à $2^{100}$
829 configurations dans le mode des itérations asynchrones.
832 La convergence des itérations asynchrones de l'exemple~\cite{BCVC10:ir} n'est pas établie
833 lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
837 \includegraphics[scale=0.6]{images/RC07ce.eps}
838 \caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE}
847 % \begin{tabular}{|*{19}{c|}}
852 % & \multicolumn{6}{|c|}{Synchronous} & \multicolumn{12}{|c|}{Asynchronous}\\
854 % Delay & \multicolumn{6}{|c|}{ }
855 % & \multicolumn{6}{|c|}
857 % & \multicolumn{6}{|c|}
858 % {Bounded+Mixed Mode}\\
860 % \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
861 % \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
862 % \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\
869 \label{sec:spin:concl}