quelques perspectives

[hdrcouchot.git] / modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index 6f968bbc292d48a37a491762ff62e7b812fed92b..191941605c1da2ba65fcc9ddff3a7e7223eb2c60 100644 (file)
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -26,7 +26,7 @@ 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}  
 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
+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 
 combinatoire, ces outils appliquent des méthodes d'ordre partiel, d'abstraction,
 de quotientage selon une relation d'équivalence.
 qu'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.


@@ -69,7 +69,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 +79,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.

   
 
 
   
 
 


@@ -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,7 +340,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.
 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
 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


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


@@ -658,7 +658,7 @@ puis présente ensuite les expérimentations issues de ce travail.
   de l'exécution en SPIN de $\psi$ est bornée par $2^{m(\delta_0+1)+n(n+2)}$.
 \end{theorem}
 \begin{Proof}
   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.
+  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.