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

diff --git a/modelchecking.tex b/modelchecking.tex
index 2a7107f..d9e626e 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -19,18 +19,19 @@ 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 
+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 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 selon 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 
@@ -38,8 +39,8 @@ 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}.
 
@@ -88,11 +89,12 @@ Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}.
 
 
 
-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 
+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}
@@ -153,7 +155,7 @@ 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Ã©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;
@@ -208,8 +210,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 
@@ -218,9 +220,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}$.
 
 
 
@@ -343,7 +345,7 @@ 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
@@ -588,7 +590,7 @@ 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. 
@@ -650,12 +652,12 @@ 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$ 
+  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)}$.
 \end{theorem}
-\begin{Proof}
+\begin{proof}
   Une configuration est une Ã©valuation des variables globales.
   Leur nombre ne dÃ©pend que de celles qui ne sont pas constantes.
 
@@ -667,11 +669,11 @@ 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.
@@ -804,10 +806,7 @@ 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.
@@ -818,7 +817,7 @@ L'exemple  \textit{RE} a Ã©tÃ© prouvÃ© comme universellement convergent.
 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
