X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/4e673fe23eacd3db39c4bc51610f1650c372b13c..02fd942d6a30fe7197b732c94450ca466b7a49f5:/modelchecking.tex?ds=inline diff --git a/modelchecking.tex b/modelchecking.tex index 6f968bb..2a7107f 100644 --- 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 @@ -26,7 +24,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} -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. @@ -43,7 +41,7 @@ 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 fournies (\Sec{sec:spin:practical}). - +Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}. @@ -69,7 +67,7 @@ sont ensuite fournies (\Sec{sec:spin:practical}). \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.} @@ -79,10 +77,10 @@ sont ensuite fournies (\Sec{sec:spin:practical}). \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 - la \Fig{fig:xplgraph} donne son graphe d'intéraction. + la \Fig{fig:xplgraph:inter:mc} donne son graphe d'intéraction. @@ -300,7 +298,7 @@ active proctype scheduler(){ } \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} @@ -340,7 +338,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}) -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 @@ -435,7 +433,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 - 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$; @@ -553,7 +551,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+. -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} @@ -658,7 +656,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} - 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. @@ -782,7 +780,7 @@ pour établir un verdict. $\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 @@ -816,7 +814,7 @@ 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. @@ -826,16 +824,13 @@ $\{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} -\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} @@ -868,7 +863,17 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle. \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.