]> AND Private Git Repository - hdrcouchot.git/blob - modelchecking.tex
Logo AND Algorithmique Numérique Distribuée

Private GIT Repository
ajout de fichiers + 15Rairo
[hdrcouchot.git] / modelchecking.tex
1
2
3
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. 
9
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.
20
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 
25 donné par l'outil. 
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.
33
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}). 
46
47
48
49
50
51
52
53 %\section{Exemple jouet}
54
55
56 \begin{figure}[ht]
57   \begin{center}
58     \subfigure[Fonction à itérer]{
59       $ F(x)= \left \{
60         \begin{array}{rcl}
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
64         \end{array}
65       \right.
66       $        
67       \label{fig:map}
68     }
69     \hfill
70     \subfigure[Graphe d'intéraction]{
71       \includegraphics[width=4cm]{images/xplCnxMc.eps}
72       \label{fig:xplgraph}
73     }
74   \end{center}
75   \caption{Exemple pour SDD $\approx$ SPIN.}
76 \end{figure}
77
78
79
80 \begin{xpl}
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} donne son graphe d'intéraction.
86   
87
88
89
90
91
92
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 
96 $x^0=7$ restent en 7.
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:
100 \begin{itemize}
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.
105 \end{itemize}   
106 \end{xpl}
107
108
109
110
111
112 \section{Rappels sur le langage PROMELA}
113 \label{sec:spin:promela}
114
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}.
117
118
119
120
121 \begin{figure}[ht]
122 \begin{tiny}
123 \begin{lstlisting}
124 #define N 3
125 #define d_0 5
126
127 bool X [N]; bool Xp [N]; int mods [N];
128 typedef vals{bool v [N]};
129 vals Xd [N];  
130
131 typedef a_send{chan sent[N]=[d_0] of {bool}};
132 a_send channels [N];
133
134 chan unlock_elements_update=[1] of {bool};
135 chan sync_mutex=[1] of {bool};
136 \end{lstlisting}
137 \end{tiny}
138 \caption{Declaration des types de la traduction.}
139 \label{fig:arrayofchannels}
140 \end{figure}
141
142
143 % Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
144 % \texttt{short} et  \texttt{int}.
145 Comme en C,
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
150 % dimensions.
151
152 \begin{xpl}
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. 
155 Il définit:
156 \begin{itemize}
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}$).
170 \end{itemize}
171
172
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.
178
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:
185 \begin{itemize}
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.
192 \end{itemize}
193 \end{xpl}
194
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 
200 \texttt{run}.
201 Parmi tous les process,  \verb+init+ est le process  initial qui permet 
202 d'initialiser les variables, lancer d'autres process\ldots
203
204
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.
216
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é.
221
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)}$.
226
227
228
229 Pour chaque  élément $i$, si les itérations sont asynchrones
230 \begin{itemize}
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]+.
240 \end{itemize}
241
242 \begin{figure}[t]
243   \begin{minipage}[h]{.32\linewidth}
244 \begin{tiny}
245 \begin{lstlisting}
246 init{
247  int i=0; int j=0; bool is_succ=0;
248  do
249  ::i==N->break;
250  ::i< N->{
251    if
252    ::Xp[i]=0;
253    ::Xp[i]=1;
254    fi;
255    j=0;
256    do
257    ::j==N -> break;
258    ::j< N -> Xd[j].v[i]=Xp[i]; j++;
259    od;
260    j=0;
261    do
262    ::j==N -> break;
263    ::j< N -> {
264      hasnext(i,j);
265      if
266      ::(i!=j && is_succ==1) -> 
267      channels[i].sent[j] ! Xp[i];
268      ::(i==j || is_succ==0) -> skip; 
269      fi;  
270      j++;}
271    od;
272    i++;}
273  od;
274  sync_mutex ! 1;
275 }
276 \end{lstlisting}
277 \end{tiny}
278 \caption{Process init.}\label{fig:spin:init} 
279 \end{minipage}\hfill
280  \begin{minipage}[h]{.32\linewidth}
281 \begin{tiny}
282 \begin{lstlisting}
283 active proctype scheduler(){ 
284  do
285  ::sync_mutex ? 1 -> {
286    int i=0; int j=0;
287    do
288    :: i==N -> break;
289    :: i< N -> {
290      if
291      ::skip;
292      ::mods[j]=i; j++;
293      fi;
294      i++;}
295    od;
296    ar_len=i; 
297    unlock_elements_update ! 1;
298    }
299  od
300 }
301 \end{lstlisting}
302 \end{tiny}
303 \caption{Process scheduler pour la stratégie pseudo pérodique.
304  \label{fig:scheduler}}
305 \end{minipage}
306 \begin{minipage}[h]{.30\linewidth}
307 \begin{tiny}
308 \begin{lstlisting}
309 inline hasnext(i,j){
310   if
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
320   fi
321 }
322 \end{lstlisting}
323 \end{tiny}
324 \caption{Codage du graphe d'intéraction de $f$.
325  \label{fig:spin:hasnext}}
326 \end{minipage}
327
328 \end{figure}
329
330
331
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.
338
339
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$.
345
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+.
353
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:
361
362 \begin{figure}[t]
363 \begin{minipage}[b]{.32\linewidth}
364 \begin{tiny}
365 \begin{lstlisting}
366 inline update_X(){      
367   int countu;
368   countu = 0;
369   do
370     :: countu == N -> break ;
371     :: countu != N ->
372        X[countu] = Xp[countu];
373        countu ++ ;
374   od
375 }
376 \end{lstlisting}
377 \end{tiny}
378 \caption{Sauvegarde de l'état courant}\label{fig:spin:sauve}
379 \end{minipage}\hfill%
380 \begin{minipage}[b]{.32\linewidth}
381 \begin{tiny}
382 \begin{lstlisting}
383 active proctype update_elems(){
384  do
385  ::unlock_elements_update ? 1 ->
386    {
387     atomic{
388      bool is_succ=0;
389      update_X();
390      fetch_values();
391      int count = 0;
392      int j = 0;
393      do
394      ::count == ar_len -> break;
395      ::count < ar_len ->
396        j = mods[count];     
397        F(j);
398        count++;
399      od;
400      diffuse_values(Xp);
401      sync_mutex ! 1
402     }
403    }
404  od
405 }
406 \end{lstlisting}
407 \end{tiny}
408 \caption{Mise à jour des éléments.}\label{fig:proc}
409   \end{minipage}\hfill%
410 %\end{figure}
411 %\begin{figure}
412   \begin{minipage}[b]{.33\linewidth}
413 \begin{tiny}
414 \begin{lstlisting}
415 inline F(){
416  if
417  ::j==0 -> Xp[0] = 
418       (Xs[j].v[0] & !Xs[j].v[1]) 
419      |(Xs[j].v[2])
420  ::j==1 -> Xp[1] =  Xs[j].v[0] 
421                  | !Xs[j].v[2]
422  ::j==2 -> Xp[2] =  Xs[j].v[1] 
423                  &  Xs[j].v[2]
424  fi
425 }
426 \end{lstlisting}
427 \end{tiny}
428 \caption{Application de la fonction $f$.}\label{fig:p}
429   \end{minipage}
430 \end{figure}
431
432
433 \begin{enumerate}
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}).
448 \end{enumerate}
449
450
451
452
453
454
455
456
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.
463
464 \begin{figure}[t]
465   \begin{minipage}[h]{.475\linewidth}
466 \begin{tiny}
467 \begin{lstlisting}
468 inline fetch_values(){
469  int countv = 0;
470  do
471  :: countv == ar_len -> break ;
472  :: countv < ar_len ->
473     j = mods[countv];
474     i = 0;       
475     do
476     :: (i == N) -> break;
477     :: (i < N && i == j) -> {
478         Xd[j].v[i] = Xp[i] ;
479         i++ }   
480     :: (i < N && i != j) -> {
481         hasnext(i,j);
482         if
483         :: skip
484         :: is_succ==1 &&
485     nempty(channels[i].sent[j]) ->
486             channels[i].sent[j] ?
487                         Xd[j].v[i];
488         fi; 
489         i++ }
490     od;
491     countv++
492  od
493 }
494 \end{lstlisting}
495 \end{tiny}
496 \caption{Récupérer les valeurs des elements\label{fig:val}}
497   \end{minipage}\hfill%
498   \begin{minipage}[h]{.475\linewidth}
499 \begin{tiny}
500 \begin{lstlisting}
501 inline diffuse_values(values){   
502  int countb=0;
503  do
504  :: countb == ar_len -> break ;
505  :: countb < ar_len ->
506     j = mods[countb];
507     i = 0 ;
508     do
509     :: (i == N) -> break;
510     :: (i < N && i == j) -> i++;   
511     :: (i < N && i != j) -> {
512         hasnext(j,i);
513         if
514         :: skip
515         :: is_succ==1 && 
516      nfull(channels[j].sent[i]) ->
517             channels[j].sent[i] ! 
518                          values[j];
519         fi;
520         i++ }
521     od;
522     countb++
523  od
524 }       
525 \end{lstlisting}
526 \end{tiny}
527 \caption{Diffuser les valeurs des elements}\label{fig:broadcast}
528   \end{minipage}
529 \end{figure}
530
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$)
535 dont $j$ dépend. 
536 Il y a deux cas.
537 \begin{itemize}
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):
542   \begin{itemize}
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).
550   \end{itemize}
551 \end{itemize}
552
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}$:
559 \begin{itemize}
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).
564 \end{itemize}
565
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 
573 délai.
574
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.
582
583 % Notice furthermore that PROMELA is an  imperative language which
584 % often results in generating  intermediate  states 
585 % (to  execute  a matrix assignment  for
586 % instance). 
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.
589
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.
594
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:
601 \begin{equation}
602 \diamond  (\Box  \verb+Xp+ = \verb+X+)
603 \label{eq:ltl:conv}
604 \end{equation}
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.
614
615
616
617 \section{Correction et complétude de la démarche}\label{sec:spin:proof}
618
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}.
624
625
626 \begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
627 \label{Theo:sound}
628 %
629   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.  
630   Si $\psi$ vérifie
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.
633 \end{restatable}
634
635
636 \begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete}
637 \label{Theo:completeness}
638 %
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.
642 \end{restatable}
643
644
645
646
647
648
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.
653
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)}$.
659 \end{theorem}
660 \begin{Proof}
661   Une configuration est une valuation des variables globales.
662   Leur nombre ne dépend que de celles qui ne sont pas constantes.
663
664   Les  variables  \verb+Xp+ et \verb+X+ engendrent  $2^{2n}$ états.
665   La variable
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$, 
673   $m$ et $\delta_0$.
674   %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
675   
676 \end{Proof}
677
678 La méthode détaillée ici a pu être appliquée sur l'exemple
679 pour prouver formellement sa convergence universelle.
680
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$:  
687 $$
688 \Box \diamond (l == l_0) \Rightarrow 
689 ((\Box \diamond (l== l_1)) \land  \ldots \land (\Box \diamond (l == l_k)))
690 $$
691
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}. 
700
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.
708
709 % \begin{xpl}
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
717 % after few minutes.
718 % All the experimentation have been realized in a classic desktop computer.
719 % \end{xpl}
720
721
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}) 
724 avec ou sans délais.
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 
727 universelle 
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.
732
733
734 \begin{figure}[ht]
735   \begin{center}
736     \begin{tiny}
737       \subfigure[Sans délais]{
738         \begin{tabular}{|*{7}{c|}}
739           \cline{2-7}
740           \multicolumn{1}{c|}{ }
741           &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Généralisées} \\
742           \cline{2-7}
743           \multicolumn{1}{c|}{ }& 
744           P & M & T&
745           P & M & T \\
746           \hline %\cline{2-7}
747           \textit{RE}  &
748           $\top$ & 2.7 & 0.01s & 
749           $\bot$ & 369.371 & 0.509s \\ 
750           \hline %\cline{2-7}
751           \cite{RC07} &
752           $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
753           $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
754           \hline
755           \cite{BM99} &
756           $\top$ & 36.7 & 12s & % BM99_sync_para.spin
757           $\top$ &  &  \\ % BM99_sync_chao.spin
758           \hline
759         \end{tabular}
760         \label{fig:sync:exp}  
761       }
762     
763       \subfigure[Avec délais]{
764         \begin{tabular}{|*{13}{c|}}
765           \cline{2-13}
766           \multicolumn{1}{c|}{ }
767           &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement borné} \\
768           \cline{2-13}
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} \\
772           \cline{2-13}
773           \multicolumn{1}{c|}{ }
774           &P & M & T &
775           P & M & T &
776           P & M & T&
777           P & M & T \\
778           \hline %cline{2-13}
779           \textit{RE} & 
780           $\top$ & 409 & 1m11s&
781           $\bot$ & 370 & 0.54 &
782           $\bot$ & 374 & 7.7s&
783           $\bot$ & 370 & 0.51s \\
784           \hline %\cline{2-13}
785           AC2D 
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 
790           \hline %\cline{2-13}
791           \cite{BM99}
792           &$\top$ &  &   %BM99_mixed_para.spin 
793           &$\top$ &  &    % RC07_async_mixed_all.spin
794           &$\bot$ &  &    % RC07_async.spin
795           &$\bot$ &  &   \\ % RC07_async_all.spin 
796           \hline %\cline{2-13}
797         \end{tabular}
798         \label{fig:async:exp}
799       }
800     \end{tiny}
801   \end{center}
802   \caption{Résultats des simulations Promela des SDDs}\label{fig:exp:promela}
803 \end{figure} 
804
805
806
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 
812 de 4 voisins et
813 \cite{BM99} consiste en  10 process
814 qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche 
815 du graphe complet.
816
817
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
827 de~\cite{BM99}, 
828 $\delta_0$ est réduit à 1. Cela aboutit cependant à $2^{100}$ 
829 configurations dans le mode des itérations asynchrones.
830
831 \JFC{Quid de ceci?}
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.
834
835 \begin{figure}
836 \centering
837 \includegraphics[scale=0.6]{images/RC07ce.eps}   
838 \caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE}
839 \end{figure}
840
841
842
843
844
845
846
847 % \begin{tabular}{|*{19}{c|}}
848 % % \hline 
849 % % e \\
850 % % 
851 % \hline
852 % & \multicolumn{6}{|c|}{Synchronous} & \multicolumn{12}{|c|}{Asynchronous}\\
853 % \cline{8-19}
854 % Delay &  \multicolumn{6}{|c|}{ }
855 % & \multicolumn{6}{|c|}
856 % {Only Bounded}
857 % & \multicolumn{6}{|c|}
858 % {Bounded+Mixed Mode}\\
859 % Strategy&
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} \\
863
864
865 %  \end{tabular}
866
867  
868 \section{Conclusion}
869 \label{sec:spin:concl}
870
871
872
873
874
875
876