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

diff --git a/modelchecking.tex b/modelchecking.tex
index ca223fb..dd4bf2e 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}
+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és, le problème 
+se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones 
+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 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 
+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 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 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 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  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érimentations
+sont ensuite fournies (\Sec{sec:spin:practical}). 
+Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}.
+
+
+
+
+
+
+%\section{Exemple jouet}
 
-\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.
-  
 \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,34 +64,43 @@
         \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 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 autres modes synchrones avec  une 
-stratégie pseudo périodique, les comportements selon la configuration initiale:
+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}   
@@ -92,59 +141,62 @@ 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$;
+ ${\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 
-(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; 
-il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $x$ à changé ou pas;
+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$ 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 
  \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$.
+ 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}
 
 %\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 
@@ -159,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 
@@ -169,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}$.
 
 
 
@@ -249,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}
@@ -287,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
@@ -304,7 +356,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:
 
@@ -354,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}
@@ -374,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$;
@@ -407,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}
@@ -486,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;
@@ -502,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 
@@ -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 
@@ -539,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
@@ -566,26 +617,31 @@ 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{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}
+
+
 
 
 
@@ -595,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.
@@ -613,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}
+  %\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 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
-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$:  
@@ -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,113 +731,105 @@ $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 Mixte} & \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}
+          \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
+          &$\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
+à valeur dans $\{0,1,2\}$ 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.
-\JFC{statuer sur AC2D}
-Comme la convergence n'est déjà pas établie pour les itérations parallèles
+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 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}
 
 
@@ -812,29 +861,19 @@ 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}. 
 
+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.