une version de plus

[hdrcouchot.git] / modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index d9e626e015fd099041e8bfa4d0bbac4aef8a96ea..dd4bf2ec337445ee1a904bbe6918a1d1636b708c 100644 (file)
--- 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 
 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 
 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,  
 
 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 
 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 
 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 
 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 
 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 
 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 
 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}
 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}   
 \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
 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; 
 \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 
 \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$;
 \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 
 \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}
 
 \end{itemize}
 \end{xpl}
 


@@ -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,14 +426,14 @@ 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}
 
 
 \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}
   \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)})
 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+.   
 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}
 
 \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]+;
 \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}
   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,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 
 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}
 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
 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
 \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,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
 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$:  
 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|}{ }
         \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} &
           \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, 
 \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.
 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 
 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