X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/f4dd79b2c3181cb26ec94555b62ed77dcb0a4200..e760413d8a2e7bc9385c7fd3e94e629b4edee6e7:/modelchecking.tex?ds=inline

diff --git a/modelchecking.tex b/modelchecking.tex
index ca223fb..1919416 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,21 +1,61 @@
-\JFC{donner dans les rappels les dÃ©lais et les propriÃ©tÃ©s de convergence universelle}
 
-\JFC{Statuer sur la taille des exemples traitables par la dÃ©marche, cf donnÃ©es pratiques}
 
-\section{Exemple jouet}
 
-\begin{xpl}
-  On considÃ¨re dans ce chapitre l'exemple oÃ¹ trois Ã©lÃ©ments dans $\Bool$. 
-  Chaque configuration est ainsi un Ã©lement de $\{0,1\}^3$, \textit{i.e.}, 
-  un nombre entre 0 et 7. 
-  La \Fig{fig:map} prÃ©cise la fonction $f$ considÃ©rÃ©e et 
-  la \Fig{fig:xplgraph} donne son graphe d'intÃ©raction.
-  
+L'Ã©tude de convergence de systÃ¨mes dynamiques discrets est simple Ã  vÃ©rifier 
+pratiquement pour le mode synchrone. Lorsqu'on introduit des stratÃ©gies 
+pseudo pÃ©riodiques pour les modes unaires et gÃ©nÃ©ralisÃ©es, le problÃ¨me 
+se complexifie. C'est pire encore lorsqu'on traite des itÃ©rations asynchrones 
+et mixes prenant de plus en compte les dÃ©lais. 
+
+Des mÃ©thodes de simulation basÃ©es sur des stratÃ©gies et des dÃ©lais gÃ©nÃ©rÃ©s alÃ©atoirement 
+ont dÃ©jÃ  Ã©tÃ© prÃ©sentÃ©es~\cite{BM99,BCV02}.
+Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un rÃ©sultat 
+formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,  
+cela ne permet que donner une intuition de convergence, pas  une preuve.
+Autant que nous sachions, aucune dÃ©marche de preuve formelle automatique 
+de convergence n'a jamais Ã©tÃ© Ã©tablie. 
+Dans le travail thÃ©orique~\cite{Cha06}, Chandrasekaran a montrÃ© que les itÃ©rations asynchrones sont convergentes 
+si et seulement si on peut construire une fonction de Lyaponov dÃ©croissante, mais il ne donne pas de mÃ©thode 
+automatique pour construire cette fonction.
+
+Un outil qui construirait automatiquement toutes 
+les transitons serait le bienvenu. 
+Pour peu qu'on Ã©tablisse la preuve de correction et de complÃ©tude de la 
+dÃ©marche, la convergence du rÃ©seau discret ne repose alors que sur le verdict 
+donnÃ© par l'outil. 
+Cependant, mÃªme pour des rÃ©seaux discrets Ã  peu d'Ã©lÃ©ments, 
+le nombre de configurations induites explose rapidement.
+Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}  
+sont des classes d'outils qui adressent le problÃ¨me de vÃ©rifier automatiquement
+qu'un modÃ¨le vÃ©rifie une propriÃ©tÃ© donnÃ©e. Pour traiter le problÃ¨me d'explosion 
+combinatoire, ces outils appliquent des mÃ©thodes d'ordre partiel, d'abstraction,
+de quotientage selon une relation d'Ã©quivalence.
+
+Ce chapitre montre comment nous simulons 
+des rÃ©seaux discrets selon toutes les sortes d'itÃ©rations pour Ã©tablir 
+formellement leur convergence (ou pas).
+Nous dÃ©butons par un exemple et faisons quelques rappels sur 
+le langage PROMELA qui est le langage du model-checker 
+SPIN~\cite{Hol03} (\Sec{sec:spin:promela}).
+Nous prÃ©sentons ensuite la dÃ©marche de traduction 
+de rÃ©seaux discrets dans PROMELA (\Sec{sec:spin:translation}).   
+Les thÃ©orÃ¨mes de correction et de complÃ©tude de la dÃ©marche
+sont ensuite donnÃ©s Ã  la (\Sec{sec:spin:proof}). 
+Des donnÃ©es pratiques comme la complexitÃ© et des synthÃ¨ses d'expÃ©rimentation
+sont ensuite fournies (\Sec{sec:spin:practical}). 
+
+
+
+
+
+
+
+%\section{Exemple jouet}
+
+
 \begin{figure}[ht]
-  \centering
-  \begin{minipage}%[h]
-    {.6\linewidth}
-    \begin{center}
+  \begin{center}
+    \subfigure[Fonction Ã  itÃ©rer]{
       $ F(x)= \left \{
         \begin{array}{rcl}
           f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3  \\
@@ -24,31 +64,39 @@
         \end{array}
       \right.
       $        
-    \end{center}
-    \caption{Fonction Ã  itÃ©rer}    \label{fig:map}
-  \end{minipage}
-  \begin{minipage}%[h]
-    {.35\linewidth}
-    \begin{center}
+      \label{fig:map}
+    }
+    \hfill
+    \subfigure[Graphe d'intÃ©raction]{
       \includegraphics[width=4cm]{images/xplCnxMc.eps}
-    \end{center}
-    \caption{Graphe d'intÃ©raction}
-    \label{fig:xplgraph}
-    \end{minipage}
+      \label{fig:xplgraph:inter:mc}
+    }
+  \end{center}
   \caption{Exemple pour SDD $\approx$ SPIN.}
 \end{figure}
 
 
 
+\begin{xpl}
+  On considÃ¨re un exemple Ã  trois Ã©lÃ©ments dans $\Bool$. 
+  Chaque configuration est ainsi un Ã©lÃ©ment de $\Bool^3$, \textit{i.e.}, 
+  un nombre entre 0 et 7. 
+  La \Fig{fig:map} prÃ©cise la fonction $f$ considÃ©rÃ©e et 
+  la \Fig{fig:xplgraph:inter:mc} donne son graphe d'intÃ©raction.
+  
+
 
 
 
-On peut facilement vÃ©rifier que toutes les itÃ©rations parallÃ¨les initialisÃ©es 
+
+
+On peut facilement vÃ©rifier que toutes les itÃ©rations synchrones initialisÃ©es 
 avec $x^0 \neq 7$ soit $(111)$ 
 convergent vers $2$ soit $(010)$; celles initialisÃ©es avec 
 $x^0=7$ restent en 7.
-Pour les autres modes synchrones avec  une 
-stratÃ©gie pseudo pÃ©riodique, les comportements selon la configuration initiale:
+Pour les  mode unaires ou gÃ©nÃ©ralisÃ©s  avec  une 
+stratÃ©gie pseudo pÃ©riodique, on a des comportements qui dÃ©pendent 
+de la configuration initiale:
 \begin{itemize}
 \item initialisÃ©e avec 7, les itÃ©rations restent en 7;
 \item initialisÃ©e avec 0, 2, 4 ou 6 les itÃ©rations convergent vers 2;
@@ -92,47 +140,50 @@ chan sync_mutex=[1] of {bool};
 \end{figure}
 
 
-Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
-\texttt{short} et  \texttt{int}. Comme dans le langage C par exemple,
-on peut dÃ©clarer des tableaux Ã  une dimension de taille constante 
+% Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
+% \texttt{short} et  \texttt{int}.
+Comme en C,
+on peut dÃ©clarer des tableaux Ã  une dimension 
 ou des nouveaux types de donnÃ©es (introduites par le mot clef 
-\verb+typedef+). Ces derniers sont utilisÃ©s pour dÃ©finir des tableaux Ã  deux
-dimensions.
+\verb+typedef+). % Ces derniers sont utilisÃ©s
+% pour dÃ©finir des tableaux Ã  deux
+% dimensions.
 
 \begin{xpl}
 Le programme donnÃ© Ã  la {\sc Figure}~\ref{fig:arrayofchannels} correspond Ã  des 
-dÃ©clarations de variables qui serviront dans l'exemple jouet de ce chapitre. 
-Il dÃ©finit tout d'abord:
+dÃ©clarations de variables qui servent dans l'exemple de ce chapitre. 
+Il dÃ©finit:
 \begin{itemize}
 \item les constantes \verb+N+ et \verb+d_0+ qui prÃ©cisent respectivement le nombre
  $n$ d'Ã©lÃ©ments et le dÃ©lais maximum $\delta_0$;
 \item les deux tableaux  (\verb+X+ et \verb+Xp+) de \verb+N+ variables boolÃ©ennes; 
 les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associÃ©es Ã  la variables $x_{i+1}$
-d'un systÃ¨me dynamique discret 
-(le dÃ©calages d'un entier est dÃ» Ã  l'indexation Ã  partir de zÃ©ro des cellules d'un tableau);
-Elles  mÃ©morisent les  valeurs de $X_{i+1}$ respectivement avant et aprÃ¨s sa mise Ã  jour; 
+d'un systÃ¨me dynamique discret;
+elles  mÃ©morisent les  valeurs de $X_{i+1}$ respectivement avant et aprÃ¨s sa mise Ã  jour; 
 il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $x$ Ã  changÃ© ou pas;
 \item le tableau \verb+mods+ contient les Ã©lÃ©ments qui doivent Ãªtre modifiÃ©s lors de l'itÃ©ration 
 en cours; cela correspond naturellement Ã  l'ensemble des Ã©lÃ©ments $s^t$;
 \item le type de donnÃ©es structurÃ©es \verb+vals+ et le tableau de tableaux 
  \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise Ã  mÃ©moriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$
- pour l'itÃ©ration au temps $t$ (en d'autres termes, utile lors du calcul de $x^{t}$).
+ pour l'itÃ©ration au temps $t$. 
+%(en d'autres termes, utile lors du calcul de $x^{t}$).
 \end{itemize}
 
 
-Puisque le dÃ©calage d'un indices ne change pas fondamentalement 
-le comportement de la version PROMELA par rapport au modÃ¨le initial
-et pour des raisons de clartÃ©, on utilisera par la suite la mÃªme 
-lettre d'indice entre les deux niveaux (pour le modÃ¨le: $x_i$ et pour  PROMELA: 
-\texttt{X[i]}). Cependant, ce dÃ©calage devra Ãªtre conservÃ© mÃ©moire.
+% Puisque le dÃ©calage d'un indices ne change pas fondamentalement 
+% le comportement de la version PROMELA par rapport au modÃ¨le initial
+% et pour des raisons de clartÃ©, on utilisera par la suite la mÃªme 
+% lettre d'indice entre les deux niveaux (pour le modÃ¨le: $x_i$ et pour  PROMELA: 
+% \texttt{X[i]}). Cependant, ce dÃ©calage devra Ãªtre conservÃ© mÃ©moire.
 
-Une donnÃ©e de type \texttt{channel} permet le 
+DÃ©clarÃ©e avec le mot clef \verb+chan+, 
+une donnÃ©e de type \texttt{channel} permet le 
 transfert de messages entre processus dans un ordre FIFO.
-Elles serait dÃ©clarÃ©e avec le mot clef \verb+chan+ suivi par sa capacitÃ© 
-(qui est constante), son nom et le type des messages qui sont stockÃ©s dans ce canal.
+% Elles serait  suivi par sa capacitÃ© 
+% (qui est constante), son nom et le type des messages qui sont stockÃ©s dans ce canal.
 Dans l'exemple prÃ©cÃ©dent, on dÃ©clare successivement:
 \begin{itemize}
-\item un canal \verb+sent+ qui vise Ã  mÃ©moriser\verb+d_0+ messages de type
+\item un canal \verb+sent+ qui vise Ã  mÃ©moriser \verb+d_0+ messages de type
  \verb+bool+; le tableau nommÃ© \verb+channels+ de \verb+N+*\verb+N+
  Ã©lÃ©ments de type \verb+a_send+ est utilisÃ© pour mÃ©moriser les valeurs intermÃ©diaires $x_j$;
  Il permet donc de temporiser leur emploi par d'autres elements $i$.
@@ -143,8 +194,8 @@ chacun un message boolÃ©en et utilisÃ© ensuite comme des sÃ©maphores.
 
 %\subsection{PROMELA Processes} 
 Le langage PROMELA exploite la notion de \emph{process} pour modÃ©liser la concurrence
-au sein de systÃ¨mes. Un process est dÃ©clarÃ© avec le mot-clÃ©
-\verb+proctype+  et est  instanciÃ© soit immÃ©diatement (lorsque sa dÃ©claration est prÃ©fixÃ©e 
+au sein de systÃ¨mes. Un process est  instanciÃ© soit immÃ©diatement
+(lorsque sa dÃ©claration est prÃ©fixÃ©e 
  par le mot-clef  \verb+active+) ou bien au moment de l'exÃ©cution de l'instruction 
 \texttt{run}.
 Parmi tous les process,  \verb+init+ est le process  initial qui permet 
@@ -249,7 +300,7 @@ active proctype scheduler(){
 }
 \end{lstlisting}
 \end{tiny}
-\caption{Process scheduler pour la stratÃ©gie pseudo pÃ©rodique.
+\caption{Process scheduler pour la stratÃ©gie pseudo pÃ©riodique.
  \label{fig:scheduler}}
 \end{minipage}
 \begin{minipage}[h]{.30\linewidth}
@@ -289,7 +340,7 @@ ces notions est traduite vers un modÃ¨le PROMELA.
 \subsection{La stratÃ©gie}\label{sub:spin:strat}
 Regardons comment une stratÃ©gie pseudo pÃ©riodique peut Ãªtre reprÃ©sentÃ©e en PROMELA.
 Intuitivement, un process \verb+scheduler+ (comme reprÃ©sentÃ© Ã  la {\sc Figure}~\ref{fig:scheduler}) 
-est iterrativement appelÃ© pour construire chaque $s^t$ reprÃ©sentant 
+est itÃ©rativement appelÃ© pour construire chaque $s^t$ reprÃ©sentant 
 les Ã©lÃ©ments possiblement mis Ã  jour Ã  l'itÃ©ration $t$.
 
 Basiquement, le process est une boucle qui est dÃ©bloquÃ©e lorsque la valeur du sÃ©maphore
@@ -304,7 +355,7 @@ suivi par des mises Ã  jour: ceci est rÃ©alisÃ© grÃ¢ce Ã  la modification de la
 La mise Ã  jour de l'ensemble  $s^t=\{s_1,\ldots, s_m\}$  des Ã©lÃ©ments qui constituent la stratÃ©gie
 $(s^t)^{t \in \Nats}$ est implantÃ©e Ã  l'aide du process  \verb+update_elems+ fourni Ã  la 
 {\sc Figure}~\ref{fig:proc}.  
-Ce process actif attend jusqu'Ã  ce qu'il soit dÃ©bloquÃ© par le process
+Ce processus actif attend jusqu'Ã  ce qu'il soit dÃ©bloquÃ© par le process
 \verb+scheduler+  Ã  l'aide du sÃ©maphore \verb+unlock_elements_update+.
 L'implantation se dÃ©roule en cinq Ã©tapes:
 
@@ -384,7 +435,7 @@ inline F(){
 \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 
 dans la section suivante;
 \item  une boucle %sur les  \texttt{ar\_len} Ã©lÃ©ments qui peuvent Ãªtre modifiÃ©s
-  met Ã  jour iterrativement la valeur de $j$ (grÃ¢ce Ã  l'appel de fonction \texttt{f(j)})
+  met Ã  jour itÃ©rativement la valeur de $j$ (grÃ¢ce Ã  l'appel de fonction \texttt{f(j)})
   pour peu que celui-ci doive Ãªtre modifiÃ©,  \textit{i.e.},   pour peu qu'il soit renseignÃ© dans
   \texttt{mods[count]}; le code source de \texttt{F} est donnÃ© en {\sc Figure}~\ref{fig:p} et est une 
   traduction directe de l'application $f$;
@@ -502,7 +553,7 @@ Il y a deux cas.
 Les valeurs des Ã©lÃ©ments sont ajoutÃ©es dans ce canal au travers de la fonction  \verb+diffuse_values+. L'objectif de cette fonction 
 est de stocker les valeurs de $x$  (reprÃ©sentÃ©
 dans le modÃ¨le par \verb+Xp+) dans le canal  \verb+channels+.
-Il permet au modÃ¨le-checker SPIN  d'exÃ©cuter 
+Il permet au model-checker SPIN  d'exÃ©cuter 
 le modÃ¨le PROMELA   comme s'il pouvait y avoir des dÃ©lais entre processus
 Il y a deux cas diffÃ©rents pour la valeur de $X_{j}$:
 \begin{itemize}
@@ -514,7 +565,7 @@ n'y a pas d'arc de $j$ Ã  $i$ dans le graphe d'incidence;
 
 L'introduction de l'indÃ©terminisme  Ã  la fois dans les fonctions \verb+fetch_values+ 
 et \verb+diffuse_values+ est nÃ©cessaire dans notre contexte. Si celui-ci n'Ã©tait 
-prÃ©sent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple rÃ©cupÃ©rer *
+prÃ©sent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple rÃ©cupÃ©rer 
 la valeur $x_i^{(t)}$ sans considÃ©rer la valeur $x_i^{(t-1)}$.  
 De maniÃ¨re duale, si le  non dÃ©terminisme  Ã©tait uniquement
 utilisÃ© dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait 
@@ -572,20 +623,25 @@ Toutes les preuves sont dÃ©placÃ©es en
 annexes~\ref{anx:promela}.
 
 
-\begin{theorem}[Correction]\label{Theo:sound}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%
   Soit $\phi$ un modÃ¨le de systÃ¨me dynamique discret et $\psi$ sa traduction PROMELA.  
   Si $\psi$ vÃ©rifie
   la propriÃ©tÃ©  LTL  (\ref{eq:ltl:conv})  sous hypothÃ¨se d'Ã©quitÃ© faible,  alors
   les itÃ©rations de $\phi$ sont universellement convergentes.
-\end{theorem}
-
+\end{restatable}
 
 
-\begin{theorem}[ComplÃ©tude]\label{Theo:completeness}
+\begin{restatable}[ComplÃ©tude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%
   Soit $\phi$ un modÃ¨le de systÃ¨me dynamique discret et $\psi$ sa traduction.  Si $\psi$ ne vÃ©rifie pas 
   la propriÃ©tÃ© LTL (\ref{eq:ltl:conv}) sous hypothÃ¨se d'Ã©quitÃ© faible,
   alors les itÃ©rations de  $\phi$ ne sont pas universellement convergentes.
-\end{theorem}
+\end{restatable}
+
+
 
 
 
@@ -602,7 +658,7 @@ puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
   de l'exÃ©cution en SPIN de $\psi$ est bornÃ©e par $2^{m(\delta_0+1)+n(n+2)}$.
 \end{theorem}
 \begin{Proof}
-  Une configuration est une valuation des variables globales.
+  Une configuration est une Ã©valuation des variables globales.
   Leur nombre ne dÃ©pend que de celles qui ne sont pas constantes.
 
   Les  variables  \verb+Xp+ et \verb+X+ engendrent  $2^{2n}$ Ã©tats.
@@ -615,11 +671,11 @@ puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
   Le nombre de configurations est donc bornÃ© par $2^{m(\delta_0+1)+n(n+2)}$.
   On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de  $n$, 
   $m$ et $\delta_0$.
-  \JFC{Donner un ordre de grandeur de cet ordre de grandeur}
+  %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
   
 \end{Proof}
 
-La mÃ©thode dÃ©taillÃ©e ici a pu Ãªtre appliquÃ©e sur l'exemple jouet
+La mÃ©thode dÃ©taillÃ©e ici a pu Ãªtre appliquÃ©e sur l'exemple
 pour prouver formellement sa convergence universelle.
 
 On peut remarquer que SPIN n'impose l'Ã©quitÃ© faible qu'entre les process
@@ -640,7 +696,7 @@ Cependant en raison de l'explosion de la taille du produit entre
 l'automate de BÃ¼chi issu de cette formule et celui issu du programme  PROMELA,
 SPIN n'arrive pas Ã  vÃ©rifier si la convergence universelle est Ã©tablie 
 ou non sur des exemples 
-simples\JFC{faire rÃ©fÃ©rence Ã  un tel exemple}. 
+simples.%\JFC{faire rÃ©fÃ©rence Ã  un tel exemple}. 
 
 Ce problÃ¨me a Ã©tÃ© pratiquement rÃ©solu en laissant SPIN 
 gÃ©nÃ©rer toutes les traces d'exÃ©cution,
@@ -664,7 +720,8 @@ Dans le cas contraire on doit analyser le contre exemple produit par SPIN.
 
 
 La mÃ©thode dÃ©taillÃ©e ici a Ã©tÃ© appliquÃ©e sur des exemples pour prouver formellement 
-leur convergence ou leur divergence (\Fig{fig:async:exp}).
+leur convergence ou leur divergence (\Fig{fig:exp:promela}) 
+avec ou sans dÃ©lais.
 Dans ces expÃ©riences, les dÃ©lais ont Ã©tÃ© bornÃ©s par $\delta_0=10$.
 Dans ce tableau,  $P$ est vrai ($\top$) si et seulement si la convergence 
 universelle 
@@ -674,95 +731,93 @@ $T$ est le temps d'exÃ©cution sur un  Intel Centrino Dual Core 2 Duo @1.8GHz ave
 pour Ã©tablir un verdict.
 
 
-\begin{figure}
-\begin{center}
-\begin{tiny}
-\begin{tabular}{|*{7}{c|}}
-\cline{2-7}
-\multicolumn{1}{c|}{ }
-&\multicolumn{3}{|c|}{ParallÃ¨les} & \multicolumn{3}{|c|}{Chaotiques} \\
-\cline{2-7}
-\multicolumn{1}{c|}{ }& 
-P & M & T&
-P & M & T \\
-\hline %\cline{2-7}
-\textit{RE}  &
-$\top$ & 2.7 & 0.01s & 
-$\bot$ & 369.371 & 0.509s \\ 
-\hline %\cline{2-7}
-\cite{RC07} &
-$\bot$ & 2.5 & 0.001s & % RC07_sync.spin
-$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
-\hline
-\cite{BM99} &
-$\top$ & 36.7 & 12s & % BM99_sync_para.spin
-$\top$ &  &  \\ % BM99_sync_chao.spin
-\hline
-\end{tabular}
-\end{tiny}
-\end{center}
-\caption{ExpÃ©rimentations avec des itÃ©rations synchrones}\label{fig:sync:exp}
-\end{figure} 
-
-
-
-\begin{figure}
-\begin{center}
-\tiny
-\begin{tabular}{|*{13}{c|}}
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
-\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&P & M & T &
-P & M & T &
-P & M & T&
-P & M & T \\
-\hline %cline{2-13}
-\textit{RE} & 
-$\top$ & 409 & 1m11s&
-$\bot$ & 370 & 0.54 &
-$\bot$ & 374 & 7.7s&
-$\bot$ & 370 & 0.51s \\
-\hline %\cline{2-13}
-AC2D 
-&$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
-&$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
-&$\bot$ & 2.5 & 0.01s   % RC07_async.spin
-&$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
-\hline %\cline{2-13}
-\cite{BM99}
-&$\top$ &  &   %BM99_mixed_para.spin 
-&$\top$ &  &    % RC07_async_mixed_all.spin
-&$\bot$ &  &    % RC07_async.spin
-&$\bot$ &  &   \\ % RC07_async_all.spin 
-\hline %\cline{2-13}
-\end{tabular}
-\end{center}
-\caption{ExpÃ©rimentations avec des itÃ©rations asynchrones}\label{fig:async:exp}
+\begin{figure}[ht]
+  \begin{center}
+    \begin{tiny}
+      \subfigure[Sans dÃ©lais]{
+        \begin{tabular}{|*{7}{c|}}
+          \cline{2-7}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{GÃ©nÃ©ralisÃ©es} \\
+          \cline{2-7}
+          \multicolumn{1}{c|}{ }& 
+          P & M & T&
+          P & M & T \\
+          \hline %\cline{2-7}
+          \textit{RE}  &
+          $\top$ & 2.7 & 0.01s & 
+          $\bot$ & 369.371 & 0.509s \\ 
+          \hline %\cline{2-7}
+          \cite{RC07} &
+          $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
+          $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
+          \hline
+          \cite{BM99} &
+          $\top$ & 36.7 & 12s & % BM99_sync_para.spin
+          $\top$ &  &  \\ % BM99_sync_chao.spin
+          \hline
+        \end{tabular}
+        \label{fig:sync:exp}  
+      }
+    
+      \subfigure[Avec dÃ©lais]{
+        \begin{tabular}{|*{13}{c|}}
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement bornÃ©} \\
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-PÃ©riodique} &
+          \multicolumn{3}{|c|} {Synchrones} & \multicolumn{3}{|c|}{Pseudo-PÃ©riodique} \\
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &P & M & T &
+          P & M & T &
+          P & M & T&
+          P & M & T \\
+          \hline %cline{2-13}
+          \textit{RE} & 
+          $\top$ & 409 & 1m11s&
+          $\bot$ & 370 & 0.54 &
+          $\bot$ & 374 & 7.7s&
+          $\bot$ & 370 & 0.51s \\
+          \hline %\cline{2-13}
+          AC2D 
+          &$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
+          &$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
+          &$\bot$ & 2.5 & 0.01s   % RC07_async.spin
+          &$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
+          \hline %\cline{2-13}
+          \cite{BM99}
+          &$\top$ &  &   %BM99_mixed_para.spin 
+          &$\top$ &  &    % RC07_async_mixed_all.spin
+          &$\bot$ &  &    % RC07_async.spin
+          &$\bot$ &  &   \\ % RC07_async_all.spin 
+          \hline %\cline{2-13}
+        \end{tabular}
+        \label{fig:async:exp}
+      }
+    \end{tiny}
+  \end{center}
+  \caption{RÃ©sultats des simulations Promela des SDDs}\label{fig:exp:promela}
 \end{figure} 
 
 
 
-L'exemple \textit{RE} est l'exemple jouet de ce chapitre,
+L'exemple \textit{RE} est l'exemple de ce chapitre,
 \cite{RC07} concerne un rÃ©seau composÃ© de deux gÃ¨nes
 Ã  valeur dans $\{0,1,2\}$,
 AC2D est un automate cellulaire  avec 9 elements prenant des
 valeurs boolÃ©ennes en fonction de 
 de 4 voisins et
 \cite{BM99} consiste en  10 process
-qui modifient leur valeur boolÃ©ennes dans un graphe d'adjacence proche 
+qui modifient leurs valeurs boolÃ©ennes dans un graphe d'adjacence proche 
 du graphe complet.
 
 
-L'exemple jouet \textit{RE} a Ã©tÃ© prouvÃ© comme universellement convergent.
+L'exemple  \textit{RE} a Ã©tÃ© prouvÃ© comme universellement convergent.
 \JFC{statuer sur AC2D}
-Comme la convergence n'est dÃ©jÃ  pas Ã©tablie pour les itÃ©rations parallÃ¨les
+Comme la convergence n'est dÃ©jÃ  pas Ã©tablie pour les itÃ©rations synchrones
 de~\cite{RC07}, il en est donc 
 de mÃªme pour les itÃ©rations asynchrones.
 La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant Ã  la violation 
@@ -812,28 +867,7 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
  
 \section{Conclusion}
 \label{sec:spin:concl}
-Des mÃ©thodes de simulation basÃ©es sur des stratÃ©gies et des dÃ©lais gÃ©nÃ©rÃ©s alÃ©atoirement 
-ont dÃ©jÃ  Ã©tÃ© prÃ©sentÃ©es~\cite{BM99,BCV02}.
-Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un rÃ©sultat 
-formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,  
-cela ne permet que donner une intuition de convergence, pas  une preuve.
-Autant que nous sachions, aucune dÃ©marche de preuve formelle automatique 
-de convergence n'a jamais Ã©tÃ© Ã©tablie. 
-Dans le travail thÃ©orique~\cite{Cha06}, Chandrasekaran a montrÃ© que les itÃ©rations asynchrones sont convergentes 
-si et seulement si on peut construire une fonction de Lyaponov dÃ©croissante, mais il ne donne pas de mÃ©thode 
-automatique pour construire cette fonction.
 
-\JFC{DÃ©placer ceci dans les perspective}
-Among drawbacks of the method,  one can argue that bounded delays is only 
-realistic in practice for close systems. 
-However, in real large scale distributed systems where bandwidth is weak, 
-this restriction is too strong. In that case, one should only consider that 
-matrix $s^{t}$ follows the  iterations of the system, \textit{i.e.},
-for all $i$, $j$, $1 \le i \le j \le n$,  we have$
-\lim\limits_{t \to \infty} s_{ij}^t = + \infty$. 
-One challenge of this work should consist in weakening this constraint. 
-We plan as future work to take into account other automatic approaches 
-to discharge proofs notably by deductive analysis~\cite{CGK05}. 
 
 
 
