X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/3759a997c005ffb313be135f98820410cb6061b4..refs/heads/master:/modelchecking.tex?ds=sidebyside

diff --git a/modelchecking.tex b/modelchecking.tex
index 96a8586..dd4bf2e 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,7 +1,8 @@
 
-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Ã©s, 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 mixtes prenant de plus en compte les dÃ©lais. 
 
@@ -95,7 +96,7 @@ 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Ã©es avec 7, les itÃ©rations restent en 7;
@@ -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,7 +426,7 @@ 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}
 
@@ -540,8 +541,7 @@ Il y a deux cas.
 \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,7 +595,7 @@ 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}
@@ -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,7 +679,7 @@ 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 
+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
