retouche preuve gray

[hdrcouchot.git] / modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index 6f968bbc292d48a37a491762ff62e7b812fed92b..d9e626e015fd099041e8bfa4d0bbac4aef8a96ea 100644 (file)
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,6 +1,4 @@
 
 

-
-

 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 
 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 


@@ -21,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 
 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}  
 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 addressent 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 
 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 
 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 


@@ -40,10 +39,10 @@ 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
 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}). 
 sont ensuite fournies (\Sec{sec:spin:practical}). 

-
+Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}.

 
 
 
 
 
 


@@ -69,7 +68,7 @@ sont ensuite fournies (\Sec{sec:spin:practical}).
     \hfill
     \subfigure[Graphe d'intéraction]{
       \includegraphics[width=4cm]{images/xplCnxMc.eps}
     \hfill
     \subfigure[Graphe d'intéraction]{
       \includegraphics[width=4cm]{images/xplCnxMc.eps}

-      \label{fig:xplgraph}
+      \label{fig:xplgraph:inter:mc}

     }
   \end{center}
   \caption{Exemple pour SDD $\approx$ SPIN.}
     }
   \end{center}
   \caption{Exemple pour SDD $\approx$ SPIN.}


@@ -79,10 +78,10 @@ sont ensuite fournies (\Sec{sec:spin:practical}).
 
 \begin{xpl}
   On considère un exemple à trois éléments dans $\Bool$. 
 
 \begin{xpl}
   On considère un exemple à trois éléments dans $\Bool$. 

-  Chaque configuration est ainsi un élement de $\Bool^3$, \textit{i.e.}, 
+  Chaque configuration est ainsi un élément de $\Bool^3$, \textit{i.e.}, 

   un nombre entre 0 et 7. 
   La \Fig{fig:map} précise la fonction $f$ considérée et 
   un nombre entre 0 et 7. 
   La \Fig{fig:map} précise la fonction $f$ considérée et 

-  la \Fig{fig:xplgraph} donne son graphe d'intéraction.
+  la \Fig{fig:xplgraph:inter:mc} donne son graphe d'intéraction.

   
 
 
   
 
 


@@ -90,11 +89,12 @@ sont ensuite fournies (\Sec{sec:spin:practical}).
 
 
 
 
 
 

-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.
 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}
 stratégie pseudo périodique, on a des comportements qui dépendent 
 de la configuration initiale:
 \begin{itemize}


@@ -155,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
 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;
 \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;


@@ -210,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
 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 
 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 


@@ -220,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}, 
 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  
 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}$.

 
 
 
 
 
 


@@ -300,7 +300,7 @@ active proctype scheduler(){
 }
 \end{lstlisting}
 \end{tiny}
 }
 \end{lstlisting}
 \end{tiny}

-\caption{Process scheduler pour la stratégie pseudo pérodique.
+\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}


@@ -340,12 +340,12 @@ 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.
 Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler}) 
 \subsection{La stratégie}\label{sub:spin:strat}
 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 iterrativement appelé pour construire chaque $s^t$ représentant 
+est itérativement appelé pour construire chaque $s^t$ représentant 

 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
 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
 \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


@@ -435,7 +435,7 @@ inline F(){
 \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 
 dans la section suivante;
 \item  une boucle %sur les  \texttt{ar\_len} éléments qui peuvent être modifiés
 \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 
 dans la section suivante;
 \item  une boucle %sur les  \texttt{ar\_len} éléments qui peuvent être modifiés

-  met à jour iterrativement la valeur de $j$ (grâce à l'appel de fonction \texttt{f(j)})
+  met à jour itérativement la valeur de $j$ (grâce à l'appel de fonction \texttt{f(j)})

   pour peu que celui-ci doive être modifié,  \textit{i.e.},   pour peu qu'il soit renseigné dans
   \texttt{mods[count]}; le code source de \texttt{F} est donné en {\sc Figure}~\ref{fig:p} et est une 
   traduction directe de l'application $f$;
   pour peu que celui-ci doive être modifié,  \textit{i.e.},   pour peu qu'il soit renseigné dans
   \texttt{mods[count]}; le code source de \texttt{F} est donné en {\sc Figure}~\ref{fig:p} et est une 
   traduction directe de l'application $f$;


@@ -553,7 +553,7 @@ Il y a deux cas.
 Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonction  \verb+diffuse_values+. L'objectif de cette fonction 
 est de stocker les valeurs de $x$  (représenté
 dans le modèle par \verb+Xp+) dans le canal  \verb+channels+.
 Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonction  \verb+diffuse_values+. L'objectif de cette fonction 
 est de stocker les valeurs de $x$  (représenté
 dans le modèle par \verb+Xp+) dans le canal  \verb+channels+.

-Il permet au modèle-checker SPIN  d'exécuter 
+Il permet au model-checker SPIN  d'exécuter 

 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}
 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}


@@ -590,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 
 \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. 
 
 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. 


@@ -652,13 +652,13 @@ 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 ]
 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}
   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}
-  Une configuration est une valuation des variables globales.
+\begin{proof}
+  Une configuration est une évaluation des variables globales.

   Leur nombre ne dépend que de celles qui ne sont pas constantes.
 
   Les  variables  \verb+Xp+ et \verb+X+ engendrent  $2^{2n}$ états.
   Leur nombre ne dépend que de celles qui ne sont pas constantes.
 
   Les  variables  \verb+Xp+ et \verb+X+ engendrent  $2^{2n}$ états.


@@ -669,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)}$.
   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}
   
   $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.
 
 La méthode détaillée ici a pu être appliquée sur l'exemple
 pour prouver formellement sa convergence universelle.


@@ -782,7 +782,7 @@ pour établir un verdict.
           $\bot$ & 374 & 7.7s&
           $\bot$ & 370 & 0.51s \\
           \hline %\cline{2-13}
           $\bot$ & 374 & 7.7s&
           $\bot$ & 370 & 0.51s \\
           \hline %\cline{2-13}

-          AC2D 
+          \cite{RC07}

           &$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
           &$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
           &$\bot$ & 2.5 & 0.01s   % RC07_async.spin
           &$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
           &$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
           &$\bot$ & 2.5 & 0.01s   % RC07_async.spin


@@ -806,36 +806,30 @@ 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
 
 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.
 
 
 L'exemple  \textit{RE} a été prouvé comme universellement convergent.
 \cite{BM99} consiste en  10 process
 qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche 
 du graphe complet.
 
 
 L'exemple  \textit{RE} a été prouvé comme universellement convergent.

-\JFC{statuer sur AC2D}
+%\JFC{statuer sur AC2D}

 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.
 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
 de~\cite{BM99}, 
 $\delta_0$ est réduit à 1. Cela aboutit cependant à $2^{100}$ 
 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
 de~\cite{BM99}, 
 $\delta_0$ est réduit à 1. Cela aboutit cependant à $2^{100}$ 

-configurations dans le mode des itérations asynchrones.
-
-\JFC{Quid de ceci?}
-La convergence des itérations asynchrones de l'exemple~\cite{BCVC10:ir} n'est pas établie 
-lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
+configurations dans le mode des itérations asynchrones, montrant les limites de
+l'approche.

 
 \begin{figure}
 \centering
 \includegraphics[scale=0.6]{images/RC07ce.eps}   
 
 \begin{figure}
 \centering
 \includegraphics[scale=0.6]{images/RC07ce.eps}   

-\caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE}
+\caption{Contre exemple de convergence pour~~\cite{RC07}} \label{fig:RC07CE}

 \end{figure}
 
 
 \end{figure}
 
 


@@ -868,7 +862,17 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
 \section{Conclusion}
 \label{sec:spin:concl}
 
 \section{Conclusion}
 \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 
+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é.
+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 
+convergent pas.