X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/2b04820abccb0772b10b2c53542ecddc6a6f600c..020defdbb2ac938563eba1071c78520973093e4b:/modelchecking.tex?ds=sidebyside diff --git a/modelchecking.tex b/modelchecking.tex index 1b8843d..6f968bb 100644 --- a/modelchecking.tex +++ b/modelchecking.tex @@ -1,21 +1,61 @@ -\JFC{donner dans les rappels les délais et les propriétés de convergence universelle} -\JFC{Statuer sur la taille des exemples traitables par la démarche, cf données pratiques} -\section{Exemple jouet} -\begin{xpl} - On considère dans ce chapitre l'exemple où trois éléments dans $\Bool$. - Chaque configuration est ainsi un élement de $\{0,1\}^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. - +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 +se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones +et mixes 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, +cela ne permet que 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 +si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode +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 +démarche, la convergence du réseau discret ne repose 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} +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 +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 +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 +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 +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}). + + + + + + + +%\section{Exemple jouet} + + \begin{figure}[ht] - \centering - \begin{minipage}%[h] - {.6\linewidth} - \begin{center} + \begin{center} + \subfigure[Fonction à itérer]{ $ F(x)= \left \{ \begin{array}{rcl} f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3 \\ @@ -24,31 +64,39 @@ \end{array} \right. $ - \end{center} - \caption{Fonction à itérer} \label{fig:map} - \end{minipage} - \begin{minipage}%[h] - {.35\linewidth} - \begin{center} + \label{fig:map} + } + \hfill + \subfigure[Graphe d'intéraction]{ \includegraphics[width=4cm]{images/xplCnxMc.eps} - \end{center} - \caption{Graphe d'intéraction} - \label{fig:xplgraph} - \end{minipage} + \label{fig:xplgraph} + } + \end{center} \caption{Exemple pour SDD $\approx$ SPIN.} \end{figure} +\begin{xpl} + On considère un exemple à trois éléments dans $\Bool$. + Chaque configuration est ainsi un élement 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. + + + + -On peut facilement vérifier que toutes les itérations parallèles initialisées +On peut facilement vérifier que toutes les itérations 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. -Pour les autres modes synchrones avec une -stratégie pseudo périodique, les comportements selon la configuration initiale: +Pour les mode 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} \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; @@ -92,47 +140,50 @@ chan sync_mutex=[1] of {bool}; \end{figure} -Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte}, -\texttt{short} et \texttt{int}. Comme dans le langage C par exemple, -on peut déclarer des tableaux à une dimension de taille constante +% Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte}, +% \texttt{short} et \texttt{int}. +Comme en C, +on peut déclarer des tableaux à une dimension ou des nouveaux types de données (introduites par le mot clef -\verb+typedef+). Ces derniers sont utilisés pour définir des tableaux à deux -dimensions. +\verb+typedef+). % Ces derniers sont utilisés +% pour définir des tableaux à deux +% dimensions. \begin{xpl} Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des -déclarations de variables qui serviront dans l'exemple jouet de ce chapitre. -Il définit tout d'abord: +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 $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 -(le décalages d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau); -Elles mémorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour; +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; \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 \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$ - pour l'itération au temps $t$ (en d'autres termes, utile lors du calcul de $x^{t}$). + pour l'itération au temps $t$. +%(en d'autres termes, utile lors du calcul de $x^{t}$). \end{itemize} -Puisque le décalage d'un indices ne change pas fondamentalement -le comportement de la version PROMELA par rapport au modèle initial -et pour des raisons de clarté, on utilisera par la suite la même -lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour PROMELA: -\texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire. +% Puisque le décalage d'un indices ne change pas fondamentalement +% le comportement de la version PROMELA par rapport au modèle initial +% et pour des raisons de clarté, on utilisera par la suite la même +% lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour PROMELA: +% \texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire. -Une donnée de type \texttt{channel} permet le +Déclarée avec le mot clef \verb+chan+, +une donnée de type \texttt{channel} permet le transfert de messages entre processus dans un ordre FIFO. -Elles serait déclarée avec le mot clef \verb+chan+ suivi par sa capacité -(qui est constante), son nom et le type des messages qui sont stockés dans ce canal. +% Elles serait suivi par sa capacité +% (qui est constante), son nom et le type des messages qui sont stockés dans ce canal. Dans l'exemple précédent, on déclare successivement: \begin{itemize} -\item un canal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type +\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$. @@ -143,8 +194,8 @@ chacun un message booléen et utilisé ensuite comme des sémaphores. %\subsection{PROMELA Processes} Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurrence -au sein de systèmes. Un process est déclaré avec le mot-clé -\verb+proctype+ et est instancié soit immédiatement (lorsque sa déclaration est préfixée +au sein de systèmes. Un process est instancié soit immédiatement +(lorsque sa déclaration est préfixée par le mot-clef \verb+active+) ou bien au moment de l'exécution de l'instruction \texttt{run}. Parmi tous les process, \verb+init+ est le process initial qui permet @@ -304,7 +355,7 @@ suivi par des mises à jour: ceci est réalisé grâce à la modification de la La mise à jour de l'ensemble $s^t=\{s_1,\ldots, s_m\}$ des éléments qui constituent la stratégie $(s^t)^{t \in \Nats}$ est implantée à l'aide du process \verb+update_elems+ fourni à la {\sc Figure}~\ref{fig:proc}. -Ce process actif attend jusqu'à ce qu'il soit débloqué par le process +Ce processus actif attend jusqu'à ce qu'il soit débloqué par le process \verb+scheduler+ à l'aide du sémaphore \verb+unlock_elements_update+. L'implantation se déroule en cinq étapes: @@ -514,7 +565,7 @@ n'y a pas d'arc de $j$ à $i$ dans le graphe d'incidence; L'introduction de l'indéterminisme à la fois dans les fonctions \verb+fetch_values+ et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était -présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer * +présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer la valeur $x_i^{(t)}$ sans considérer la valeur $x_i^{(t-1)}$. De manière duale, si le non déterminisme était uniquement utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait @@ -620,11 +671,11 @@ puis présente ensuite les expérimentations issues de ce travail. 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$, $m$ et $\delta_0$. - \JFC{Donner un ordre de grandeur de cet ordre de grandeur} + %\JFC{Donner un ordre de grandeur de cet ordre de grandeur} \end{Proof} -La méthode détaillée ici a pu être appliquée sur l'exemple jouet +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 @@ -645,7 +696,7 @@ Cependant en raison de l'explosion de la taille du produit entre l'automate de Büchi issu de cette formule et celui issu du programme PROMELA, SPIN n'arrive pas à vérifier si la convergence universelle est établie ou non sur des exemples -simples\JFC{faire référence à un tel exemple}. +simples.%\JFC{faire référence à un tel exemple}. Ce problème a été pratiquement résolu en laissant SPIN générer toutes les traces d'exécution, @@ -669,7 +720,8 @@ Dans le cas contraire on doit analyser le contre exemple produit par SPIN. La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement -leur convergence ou leur divergence (\Fig{fig:async:exp}). +leur convergence ou leur divergence (\Fig{fig:exp:promela}) +avec ou sans délais. Dans ces expériences, les délais ont été bornés par $\delta_0=10$. Dans ce tableau, $P$ est vrai ($\top$) si et seulement si la convergence universelle @@ -679,95 +731,93 @@ $T$ est le temps d'exécution sur un Intel Centrino Dual Core 2 Duo @1.8GHz ave pour établir un verdict. -\begin{figure} -\begin{center} -\begin{tiny} -\begin{tabular}{|*{7}{c|}} -\cline{2-7} -\multicolumn{1}{c|}{ } -&\multicolumn{3}{|c|}{Parallèles} & \multicolumn{3}{|c|}{Chaotiques} \\ -\cline{2-7} -\multicolumn{1}{c|}{ }& -P & M & T& -P & M & T \\ -\hline %\cline{2-7} -\textit{RE} & -$\top$ & 2.7 & 0.01s & -$\bot$ & 369.371 & 0.509s \\ -\hline %\cline{2-7} -\cite{RC07} & -$\bot$ & 2.5 & 0.001s & % RC07_sync.spin -$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin -\hline -\cite{BM99} & -$\top$ & 36.7 & 12s & % BM99_sync_para.spin -$\top$ & & \\ % BM99_sync_chao.spin -\hline -\end{tabular} -\end{tiny} -\end{center} -\caption{Expérimentations avec des itérations synchrones}\label{fig:sync:exp} -\end{figure} - - - -\begin{figure} -\begin{center} -\tiny -\begin{tabular}{|*{13}{c|}} -\cline{2-13} -\multicolumn{1}{c|}{ } -&\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\ -\cline{2-13} -\multicolumn{1}{c|}{ } -&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} & -\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\ -\cline{2-13} -\multicolumn{1}{c|}{ } -&P & M & T & -P & M & T & -P & M & T& -P & M & T \\ -\hline %cline{2-13} -\textit{RE} & -$\top$ & 409 & 1m11s& -$\bot$ & 370 & 0.54 & -$\bot$ & 374 & 7.7s& -$\bot$ & 370 & 0.51s \\ -\hline %\cline{2-13} -AC2D -&$\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.01s \\ % RC07_async_all.spin -\hline %\cline{2-13} -\cite{BM99} -&$\top$ & & %BM99_mixed_para.spin -&$\top$ & & % RC07_async_mixed_all.spin -&$\bot$ & & % RC07_async.spin -&$\bot$ & & \\ % RC07_async_all.spin -\hline %\cline{2-13} -\end{tabular} -\end{center} -\caption{Expérimentations avec des itérations asynchrones}\label{fig:async:exp} +\begin{figure}[ht] + \begin{center} + \begin{tiny} + \subfigure[Sans délais]{ + \begin{tabular}{|*{7}{c|}} + \cline{2-7} + \multicolumn{1}{c|}{ } + &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Généralisées} \\ + \cline{2-7} + \multicolumn{1}{c|}{ }& + P & M & T& + P & M & T \\ + \hline %\cline{2-7} + \textit{RE} & + $\top$ & 2.7 & 0.01s & + $\bot$ & 369.371 & 0.509s \\ + \hline %\cline{2-7} + \cite{RC07} & + $\bot$ & 2.5 & 0.001s & % RC07_sync.spin + $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin + \hline + \cite{BM99} & + $\top$ & 36.7 & 12s & % BM99_sync_para.spin + $\top$ & & \\ % BM99_sync_chao.spin + \hline + \end{tabular} + \label{fig:sync:exp} + } + + \subfigure[Avec délais]{ + \begin{tabular}{|*{13}{c|}} + \cline{2-13} + \multicolumn{1}{c|}{ } + &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement borné} \\ + \cline{2-13} + \multicolumn{1}{c|}{ } + &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} & + \multicolumn{3}{|c|} {Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} \\ + \cline{2-13} + \multicolumn{1}{c|}{ } + &P & M & T & + P & M & T & + P & M & T& + P & M & T \\ + \hline %cline{2-13} + \textit{RE} & + $\top$ & 409 & 1m11s& + $\bot$ & 370 & 0.54 & + $\bot$ & 374 & 7.7s& + $\bot$ & 370 & 0.51s \\ + \hline %\cline{2-13} + AC2D + &$\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.01s \\ % RC07_async_all.spin + \hline %\cline{2-13} + \cite{BM99} + &$\top$ & & %BM99_mixed_para.spin + &$\top$ & & % RC07_async_mixed_all.spin + &$\bot$ & & % RC07_async.spin + &$\bot$ & & \\ % RC07_async_all.spin + \hline %\cline{2-13} + \end{tabular} + \label{fig:async:exp} + } + \end{tiny} + \end{center} + \caption{Résultats des simulations Promela des SDDs}\label{fig:exp:promela} \end{figure} -L'exemple \textit{RE} est l'exemple jouet de ce chapitre, +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 \cite{BM99} consiste en 10 process -qui modifient leur valeur booléennes dans un graphe d'adjacence proche +qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche du graphe complet. -L'exemple jouet \textit{RE} a été prouvé comme universellement convergent. +L'exemple \textit{RE} a été prouvé comme universellement convergent. \JFC{statuer sur AC2D} -Comme la convergence n'est déjà pas établie pour les itérations parallèles +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 @@ -817,28 +867,7 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle. \section{Conclusion} \label{sec:spin:concl} -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. -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 -si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode -automatique pour construire cette fonction. -\JFC{Déplacer ceci dans les perspective} -Among drawbacks of the method, one can argue that bounded delays is only -realistic in practice for close systems. -However, in real large scale distributed systems where bandwidth is weak, -this restriction is too strong. In that case, one should only consider that -matrix $s^{t}$ follows the iterations of the system, \textit{i.e.}, -for all $i$, $j$, $1 \le i \le j \le n$, we have$ -\lim\limits_{t \to \infty} s_{ij}^t = + \infty$. -One challenge of this work should consist in weakening this constraint. -We plan as future work to take into account other automatic approaches -to discharge proofs notably by deductive analysis~\cite{CGK05}.