une version de plus

[hdrcouchot.git] / modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index 96a85865e9e59264441c042f6f7bdaba7b67d8c0..dd4bf2ec337445ee1a904bbe6918a1d1636b708c 100644 (file)
--- 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 
 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. 
 
 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 
 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;
 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}
 }
 \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}
  \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}
 
 
 \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$.
 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}
 }
 \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}
   \end{minipage}\hfill%
 %\end{figure}
 %\begin{figure}


@@ -425,7 +426,7 @@ inline F(){
 }
 \end{lstlisting}
 \end{tiny}
 }
 \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}
 
   \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 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;
     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 
 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 
 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 
 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}
 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
 \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 
 (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}
 
 
 \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.
 
 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 
   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.
 \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
 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
 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