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

diff --git a/modelchecking.tex b/modelchecking.tex
index 0ee325e..dd4bf2e 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,17 +1,16 @@
 
-
-
-L'Ã©tude de convergence de systÃ¨mes dynamiques discrets est simple Ã  vÃ©rifier 
+Sur des petits exemples, 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 
+pseudo-pÃ©riodiques pour les modes unaires et gÃ©nÃ©ralisÃ©s, 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. 
+et mixtes 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.
+cela ne permet que de 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 
@@ -19,20 +18,21 @@ si et seulement si on peut construire une fonction de Lyaponov dÃ©croissante, ma
 automatique pour construire cette fonction.
 
 Un outil qui construirait automatiquement toutes 
-les transitons serait le bienvenu. 
+les transitions 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 
+dÃ©marche, la convergence du rÃ©seau discret ne reposerait
+ 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 addressent 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 
+sont des classes d'outils qui adressent le problÃ¨me de dÃ©tecter automatiquement
+si 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 
+des rÃ©seaux discrets  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 
@@ -40,10 +40,10 @@ 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 donnÃ©s Ã  la \Sec{sec:spin:proof}. 
+Des donnÃ©es pratiques comme la complexitÃ© et des synthÃ¨ses d'expÃ©rimentations
 sont ensuite fournies (\Sec{sec:spin:practical}). 
-
+Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}.
 
 
 
@@ -79,7 +79,7 @@ sont ensuite fournies (\Sec{sec:spin:practical}).
 
 \begin{xpl}
   On considÃ¨re un exemple Ã  trois Ã©lÃ©ments dans $\Bool$. 
-  Chaque configuration est ainsi un Ã©lement de $\Bool^3$, \textit{i.e.}, 
+  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.
@@ -90,16 +90,17 @@ sont ensuite fournies (\Sec{sec:spin:practical}).
 
 
 
-On peut facilement vÃ©rifier que toutes les itÃ©rations synchrones initialisÃ©es 
+On peut facilement vÃ©rifier que toutes les itÃ©rations parallÃ¨les 
+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  mode unaires ou gÃ©nÃ©ralisÃ©s  avec  une 
-stratÃ©gie pseudo pÃ©riodique, on a des comportements qui dÃ©pendent 
+Pour les  modes 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;
+\item initialisÃ©es avec 7, les itÃ©rations restent en 7;
+\item initialisÃ©es avec 0, 2, 4 ou 6 les itÃ©rations convergent vers 2;
 \item initialisÃ©es avec 1, 3 ou 5, les itÃ©rations convergent vers un des 
 deux points fixes 2 ou 7.
 \end{itemize}   
@@ -155,12 +156,12 @@ 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$;
+ ${\mathsf{N}}$ d'Ã©lÃ©ments et le dÃ©lai 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;
 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;
+il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $x$ a 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 
@@ -186,9 +187,9 @@ Dans l'exemple prÃ©cÃ©dent, on dÃ©clare successivement:
 \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$.
+ Il permet donc de temporiser leur emploi par d'autres Ã©lÃ©ments $i$.
 \item les deux canaux  \verb+unlock_elements_update+ et  \verb+sync_mutex+ contenant 
-chacun un message boolÃ©en et utilisÃ© ensuite comme des sÃ©maphores.
+chacun un message boolÃ©en et sont utilisÃ©s ensuite comme des sÃ©maphores.
 \end{itemize}
 \end{xpl}
 
@@ -210,8 +211,8 @@ rÃ©ception de messages. Pour un canal
 L'instruction de rÃ©ception consomme la valeur en tÃªte du canal \verb+ch+
 et l'affecte Ã  la variable \verb+m+ (pour peu que  \verb+ch+ soit initialisÃ© et non vide).
 De maniÃ¨re similaire, l'instruction d'envoi ajoute la valeur de \verb+m+ Ã  la queue du canal
-\verb+ch+ (pour peu que celui-ci soit initialisÃ© et non rempli).
-Dans les cas problÃ©matiques, canal non initialisÃ© et vide pour une rÃ©ception ou bien rempli pour un envoi,
+\verb+ch+ (pour peu que celui-ci soit initialisÃ© et pas plein).
+Dans les cas problÃ©matiques, canal non initialisÃ© et vide pour une rÃ©ception ou plein pour un envoi,
 le processus est bloquÃ© jusqu'Ã  ce que les  conditions soient  remplies.
 
 La structures de contrÃ´le   \verb+if+   (resp.   \verb+do+)   dÃ©finit un choix non dÃ©terministe 
@@ -220,9 +221,9 @@ si plus d'une des conditions est Ã©tablie, l'ensemble des instructions correspon
 sera choisi alÃ©atoirement puis exÃ©cutÃ©.
 
 Dans le process \verb+init+ dÃ©taillÃ© Ã  la {\sc Figure}~\ref{fig:spin:init}, 
-une boucle de taille $N$ initialise alÃ©atoirement la variable  globale de type tableau \verb+Xp+.
+une boucle de taille ${\mathsf{N}}$ initialise alÃ©atoirement la variable  globale de type tableau \verb+Xp+.
 Ceci permet par la suite de vÃ©rifier si les itÃ©rations sont  convergentes pour n'importe  
-quelle configuration initiale $x^{(0)}$.
+quelle configuration initiale $x^{0}$.
 
 
 
@@ -300,7 +301,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}
@@ -338,14 +339,14 @@ 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.
+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
 \verb+sync_mutex+ est 1. Dans ce cas, les Ã©lÃ©ments Ã  modifier sont choisis
-alÃ©atoirement  (grÃ¢ce Ã   $n$ choix successifs) et sont mÃ©morisÃ©s dans le tableau
+alÃ©atoirement  (grÃ¢ce Ã   ${\mathsf{N}}$ choix successifs) et sont mÃ©morisÃ©s dans le tableau
 \verb+mods+,  dont la taille est  \verb+ar_len+.   
 Dans la sÃ©quence d'exÃ©cution, le choix d'un Ã©lÃ©ment mis Ã  jour est directement
 suivi par des mises Ã  jour: ceci est rÃ©alisÃ© grÃ¢ce Ã  la modification de la valeur du sÃ©maphore
@@ -405,7 +406,7 @@ active proctype update_elems(){
 }
 \end{lstlisting}
 \end{tiny}
-\caption{Mise Ã  jour des Ã©lÃ©ments.}\label{fig:proc}
+\caption{Mise Ã  jour des Ã©lÃ©ments}\label{fig:proc}
   \end{minipage}\hfill%
 %\end{figure}
 %\begin{figure}
@@ -425,17 +426,17 @@ inline F(){
 }
 \end{lstlisting}
 \end{tiny}
-\caption{Application de la fonction $f$.}\label{fig:p}
+\caption{Application de la fonction $f$}\label{fig:p}
   \end{minipage}
 \end{figure}
 
 
 \begin{enumerate}
 \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}
-\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 
+\item elle mÃ©morise dans  \texttt{Xd} la valeur 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$;
@@ -458,8 +459,8 @@ dans la section suivante;
 Cette  section montre comment les dÃ©lais inhÃ©rents au mode asynchrone sont 
 traduits dans le modÃ¨le  PROMELA  grÃ¢ce Ã  deux 
 fonctions \verb+fetch_values+  et   \verb+diffuse_values+.   
-Celles-ci sont donnÃ©es en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast}, 
-qui rÃ©cupÃ¨rent et diffusent respectivement les valeurs des elements.
+Celles-ci sont donnÃ©es en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast}. 
+Elles rÃ©cupÃ¨rent et diffusent respectivement les valeurs des Ã©lÃ©ments.
 
 \begin{figure}[t]
   \begin{minipage}[h]{.475\linewidth}
@@ -537,11 +538,10 @@ Il y a deux cas.
 \begin{itemize}
 \item puisque $i$ connaÃ®t sa derniÃ¨re valeur (\textit{i.e.},  $D^t_{ii}$ est toujours $t$)
   \verb+Xd[i].v[i]+ est donc  \verb+Xp[i]+;
-\item sinon, il y a deux sous cas qui peuvent peuvent potentiellement modifier la valeur 
+\item sinon, il y a deux sous-cas qui peuvent peuvent potentiellement modifier la valeur 
   que $j$ a de $i$ (et qui peuvent Ãªtre choisies de maniÃ¨re alÃ©atoire):
   \begin{itemize}
-  \item  depuis la perspective de $j$ la valeur de  $i$ peut ne pas avoir changÃ©  (
-    c'est l'instruction \verb+skip+) ou n'est pas utile; ce dernier cas apparaÃ®t 
+  \item  depuis la perspective de $j$ la valeur de  $i$ peut ne pas avoir changÃ©  (c'est l'instruction \verb+skip+) ou n'est pas utile; ce dernier cas apparaÃ®t 
     lorsqu'il n'y a pas d'arc de  $i$ Ã  $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque
     la valeur de \verb+is_succ+ qui est calculÃ©e par  \verb+hasnext(i,j)+ est 0;
     dans ce cas, la valeur de \verb+Xd[j].v[i]+ n'est pas modifiÃ©e;
@@ -553,8 +553,8 @@ 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 
-le modÃ¨le PROMELA   comme s'il pouvait y avoir des dÃ©lais entre processus
+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}
 \item soit elle est \og perdue\fg{}, \og oubliÃ©e\fg{} pour permettre Ã  $i$ de ne pas tenir compte d'une 
@@ -590,19 +590,19 @@ dÃ©lai.
 \subsection{PropriÃ©tÃ© de convergence universelle}
 Il reste Ã  formaliser dans le model checker SPIN le fait que les 
 itÃ©rations d'un systÃ¨me 
-dynamique Ã  $n$ Ã©lÃ©ments est universellement convergent.
+dynamique Ã  ${\mathsf{N}}$ Ã©lÃ©ments est universellement convergent.
 
 Rappelons tout d'abord que les variables \verb+X+  et \verb+Xp+ 
 contiennent respectivement la valeur de $x$ avant et aprÃ¨s la mise Ã  jour. 
 Ainsi, si l'on effectue une initialisation  non dÃ©terministe de 
-\verb+Xp+  et si l'on applique une stratÃ©gie pseudo pÃ©riodique,  
+\verb+Xp+  et si l'on applique une stratÃ©gie pseudo-pÃ©riodique,  
 il est nÃ©cessaire et suffisant
 de prouver la formule temporelle linÃ©aire (LTL) suivante:
 \begin{equation}
 \diamond  (\Box  \verb+Xp+ = \verb+X+)
 \label{eq:ltl:conv}
 \end{equation}
-oÃ¹ les opÃ©rateur  $\diamond$ et  $\Box$ ont
+oÃ¹ les opÃ©rateurs  $\diamond$ et  $\Box$ ont
 la sÃ©mantique usuelle, Ã  savoir
 respectivement {\em Ã©ventuellement} et {\em toujours} dans les chemins suivants.
 On note que cette propriÃ©tÃ©, si elle est Ã©tablie, garantit
@@ -617,10 +617,10 @@ disposer de plusieurs points fixes.
 \section{Correction et complÃ©tude de la dÃ©marche}\label{sec:spin:proof}
 
 Cette section prÃ©sente les thÃ©orÃ¨mes
-de correction et de  complÃ©tude de l'approche.
+de correction et de  complÃ©tude de l'approche
 (ThÃ©orÃ¨mes~\ref{Theo:sound} et~\ref{Theo:completeness}). 
 Toutes les preuves sont dÃ©placÃ©es en 
-annexes~\ref{anx:promela}.
+annexe~\ref{anx:promela}.
 
 
 \begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
@@ -651,14 +651,14 @@ annexes~\ref{anx:promela}.
 Cette section donne tout d'abord quelques mesures de complexitÃ© de l'approche 
 puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
 
-\begin{theorem}[Nombre d'Ã©tats ]
-  Soit  $\phi$  un modÃ¨le de systÃ¨me dynamique discret Ã   $n$ Ã©lÃ©ments, $m$ 
+\begin{theorem}[Nombre d'Ã©tats]
+  Soit  $\phi$  un modÃ¨le de systÃ¨me dynamique discret Ã   ${\mathsf{N}}$ Ã©lÃ©ments, $m$ 
   arcs dans le graphe d'incidence
   et $\psi$ sa traduction en PROMELA.  Le nombre de configurations 
-  de l'exÃ©cution en SPIN de $\psi$ est bornÃ©e par $2^{m(\delta_0+1)+n(n+2)}$.
+  de l'exÃ©cution en SPIN de $\psi$ est bornÃ© par $2^{m(\delta_0+1)+n(n+2)}$.
 \end{theorem}
-\begin{Proof}
-  Une configuration est une valuation des variables globales.
+\begin{proof}
+  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.
@@ -669,18 +669,18 @@ puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
   Puisque le nombre d'arÃªtes du graphe d'incidence  est $m$,  
   il y a  $m$ canaux non constants,  ce qui gÃ©nÃ¨re approximativement $2^{m(\delta_0+1)}$ Ã©tats. 
   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$, 
+  On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de  ${\mathsf{N}}$, 
   $m$ et $\delta_0$.
   %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
   
-\end{Proof}
+\end{proof}
 
 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
-alors que les preuves des deux thÃ©orÃ¨mes prÃ©cÃ©dentes reposent sur le fait que 
-celle-ci est Ã©tablie dÃ¨s qu'un choix indÃ©terministe est effectuÃ©.
+alors que les preuves des deux thÃ©orÃ¨mes prÃ©cÃ©dents reposent sur le fait que 
+cette Ã©quitÃ© est Ã©tablie dÃ¨s qu'un choix indÃ©terministe est effectuÃ©.
 NaÃ¯vement, on pourrait considÃ©rer comme hypothÃ¨se la formule suivante 
 chaque fois qu'un choix indÃ©terministe se produit entre $k$ Ã©vÃ©nements
 respectivement notÃ©s $l_1$, \ldots $l_k$:  
@@ -764,7 +764,7 @@ pour Ã©tablir un verdict.
         \begin{tabular}{|*{13}{c|}}
           \cline{2-13}
           \multicolumn{1}{c|}{ }
-          &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement bornÃ©} \\
+          &\multicolumn{6}{|c|}{Mode Mixte} & \multicolumn{6}{|c|}{Seulement bornÃ©} \\
           \cline{2-13}
           \multicolumn{1}{c|}{ }
           &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-PÃ©riodique} &
@@ -782,7 +782,7 @@ pour Ã©tablir un verdict.
           $\bot$ & 374 & 7.7s&
           $\bot$ & 370 & 0.51s \\
           \hline %\cline{2-13}
-          AC2D 
+          \cite{RC07}
           &$\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
@@ -806,36 +806,30 @@ pour Ã©tablir un verdict.
 
 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
+Ã  valeur dans $\{0,1,2\}$ et
 \cite{BM99} consiste en  10 process
 qui modifient leurs valeurs boolÃ©ennes dans un graphe d'adjacence proche 
 du graphe complet.
 
 
 L'exemple  \textit{RE} a Ã©tÃ© prouvÃ© comme universellement convergent.
-\JFC{statuer sur AC2D}
+%\JFC{statuer sur AC2D}
 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 
+La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN  menant Ã  la violation 
 de la convergence. Celle-ci correspond Ã  une stratÃ©gie pÃ©riodique qui rÃ©pÃ¨te
 $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et dÃ©bute avec $x=(0,0)$.
 En raison de la dÃ©pendance forte entre les Ã©lÃ©ments
 de~\cite{BM99}, 
 $\delta_0$ est rÃ©duit Ã  1. Cela aboutit cependant Ã  $2^{100}$ 
-configurations dans le mode des itÃ©rations asynchrones.
-
-\JFC{Quid de ceci?}
-La convergence des itÃ©rations asynchrones de l'exemple~\cite{BCVC10:ir} n'est pas Ã©tablie 
-lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
+configurations dans le mode des itÃ©rations asynchrones, montrant les limites de
+l'approche.
 
 \begin{figure}
 \centering
 \includegraphics[scale=0.6]{images/RC07ce.eps}   
-\caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE}
+\caption{Contre exemple de convergence pour~~\cite{RC07}} \label{fig:RC07CE}
 \end{figure}
 
 
@@ -868,7 +862,18 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
 \section{Conclusion}
 \label{sec:spin:concl}
 
-
+L'idÃ©e principale de ce chapitre est que l'on peut, 
+pour des rÃ©seaux boolÃ©ens Ã  dÃ©lais bornÃ©s de  petite taille, obtenir 
+une preuve de la convergence ou de sa divergence et ce
+de maniÃ¨re automatique.  
+L'idÃ©e principale est de traduire le rÃ©seau en PROMELA et de laisser 
+le model checker Ã©tablir la preuve.
+Toute l'approche a Ã©tÃ© prouvÃ©e: le verdict rendu par l'approche 
+a donc valeur de vÃ©ritÃ©.
+L'approche a cependant ses limites et ne peut donc pas Ãªtre 
+apliquÃ©e qu'Ã  des modÃ¨les simplifiÃ©s de programmes.
+La suite de ce travail consiste Ã  se focaliser sur les systÃ¨mes qui ne 
+convergent pas.
 
 
 
