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

diff --git a/modelchecking.tex b/modelchecking.tex
index d9e626e..dd4bf2e 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,15 +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 
@@ -17,7 +18,7 @@ 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 reposerait
  alors que sur le verdict 
@@ -31,7 +32,7 @@ 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 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 
@@ -95,11 +96,11 @@ avec $x^0 \neq 7$ soit $(111)$
 convergent vers $2$ soit $(010)$; celles initialisÃ©es avec 
 $x^0=7$ restent en 7.
 Pour les  modes unaires ou gÃ©nÃ©ralisÃ©s  avec  une 
-stratÃ©gie pseudo pÃ©riodique, on a des comportements qui dÃ©pendent 
+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
- ${\mathsf{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}
 
@@ -300,7 +301,7 @@ active proctype scheduler(){
 }
 \end{lstlisting}
 \end{tiny}
-\caption{Process scheduler pour la stratÃ©gie pseudo pÃ©riodique.
+\caption{Process scheduler pour la stratÃ©gie pseudo-pÃ©riodique.
  \label{fig:scheduler}}
 \end{minipage}
 \begin{minipage}[h]{.30\linewidth}
@@ -338,7 +339,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.
+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 itÃ©rativement appelÃ© pour construire chaque $s^t$ reprÃ©sentant 
 les Ã©lÃ©ments possiblement mis Ã  jour Ã  l'itÃ©ration $t$.
@@ -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,14 +426,14 @@ 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 itÃ©rativement la valeur de $j$ (grÃ¢ce Ã  l'appel de fonction \texttt{f(j)})
@@ -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;
@@ -554,7 +554,7 @@ Les valeurs des Ã©lÃ©ments sont ajoutÃ©es dans ce canal au travers de la fonctio
 est de stocker les valeurs de $x$  (reprÃ©sentÃ©
 dans le modÃ¨le par \verb+Xp+) dans le canal  \verb+channels+.
 Il permet au model-checker SPIN  d'exÃ©cuter 
-le modÃ¨le PROMELA   comme s'il pouvait y avoir des dÃ©lais entre processus
+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 
@@ -595,14 +595,14 @@ 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,11 +651,11 @@ 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 ]
+\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.
@@ -679,8 +679,8 @@ 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} &
@@ -863,12 +863,13 @@ l'approche.
 \label{sec:spin:concl}
 
 L'idÃ©e principale de ce chapitre est que l'on peut, 
-pour des rÃ©seaux boulÃ©ens Ã  dÃ©lais bornÃ©s de  petite taille, obtenir 
+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 a donc valeur de vÃ©ritÃ©.
+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 
